Time in State Machines

• Autorzy: Graf S. , Prinz A.
• Języki publikacji: EN

Abstrakty

EN

State machines are a very general means to express computations in an implementation-independent way. There are ways to extend the abstract state machine (ASM) framework with distribution aspects, but there is no unifying framework for handling time so far. We propose event structures extended with time as a natural framework for representing state machines and their true concurrency model at a semantic level and for discussing associated time models. Constraints on these timed event structures and their traces (runs) are then used for characterising different frameworks for timed computations. This characterisation of timed frameworks is independent of ASM and allows to compare time models of different modelling formalisms. Finally, we propose some specific extensions of ASM for the expressions of time constraints in accordance with the event-based semantic framework and show the applicability of the obtained framework on an example with a standard time model and a set of consistency properties for timed computations.

Słowa kluczowe

EN

abstract state machines; time model; event structures; partial order semantics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 77, nr 1,2
• Strony: 143--174
• Opis fizyczny: bibliogr. 72 poz.

Twórcy

autor

Graf S.

autor

Prinz A.

• Verimag, 2, avenue de Vingate, Grenoble, France,

Bibliografia

• [1] Abrial, J.-R., Lee, M. K. O., Neilson, D., Scharbach, P. N., Sørensen, I. H.: The B-Method., VDM Europe (2), LNCS 552, 1991.
• [2] Alpern, B., Schneider, F.: Recognizing Safety and Liveness, Distributed Computing, 2, 1987, 117-126.
• [3] Altisen, K., Tripakis, S.: Implementation of Timed Automata: An Issue of Semantics or Modeling?, Formal Modeling and Analysis of Timed Systems, Third Intl Conf. FORMATS 2005, Uppsala, Sweden, LNCS 3829, 2005.
• [4] Alur, R., Courcoubetis, C., Dill, D.: Model Checking for Real Time Systems, 5th annual IEEE Symposium on Logic in Computer Science, Philadelphia, June 1990.
• [5] Alur, R., Courcoubetis, C., Henzinger, T. A., Ho, P.-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems, Hybrid Systems 1992, LNCS 736, 1993.
• [6] Alur, R., Dill, D.: A Theory of Timed Automata, Theoretical Computer Science, 126, 1994, 183-235.
• [7] Alur, R., Henzinger, T. A.: A Really Temporal Logic, 30th Symposium on Foundations of Computer Science (FOCS 89), IEEE, 1989.
• [8] Ashenden, P. J.: The VHDL Cookbook. First Edition, Dept. Computer Science University of Adelaide South Australia, 1990.
• [9] Baier, C., Katoen, J.-P., Latella, D.: Metric Semantics for True Concurrent Real Time., Automata, Languages and Programming, 25th International Colloquium, ICALP'98, Aalborg, LNCS 1443, 1998.
• [10] Baier, C., Majster-Cederbaum, M. E.: Metric Semantics from Partial Order Semantics., Acta Inf., 34(9), 1997, 701-735.
• [11] Beauquier, D., Slissenko, A.: On Semantics of Algorithms with Continuous Time, Technical Report 97-15, Department of Informatics, Université Paris-12, 1997.
• [12] Beauquier, D., Slissenko, A.: A First Order Logic for Specification of Timed Algorithms: Basic Properties and a Decidable Class, Annals of Pure and Applied Logic, 113(1-3), 2002, 13-52.
• [13] Bednarczyk,M.: Categories of Asynchronous Systems, Phd thesis in Computer Science, University of Sussex, 1988.
• [14] Ben-Ari, M., Manna, Z., Pnueli, A.: The Temporal Logic of Branching Time, Acta Informatica, 20, 1983.
• [15] Benveniste, A., Le Guernic, P., Halbwachs, N.: A Decade of Concurrency, Reflexions and Perspeptives, REX Symposium, LNCS 803, 1993.
• [16] Bergstra, J. A., Ponse, A., SmolkaS. A., Ed.: Handbook of Process Algebra, Elsevier, ISBN: 0-444-82830-3, 2001.
• [17] Börger, E.: The ASM Refinement Method, Formal Asp. of Comput., 15(2-3), 2003, 237-257.
• [18] Börger, E., Fruja, G., Gervasi, V., Stärk, R.: A High-Level Modular Definition of the Semantics of C#,Theoretical Computer Science, 336(2-3), 2004, 235-284.
• [19] Börger, E., Gurevich, Y., Rosenzweig, D.: The Bakery Algorithm: Yet Another Specification and Verification, in: Specification and Validation Methods (E. Börger, Ed.), Oxford University Press, 1995, 231-243.
• [20] Börger, E., Stärk, R.: Abstract State Machines - A Method for High-Level System Design and Analysis, Springer Verlag, 2003.
• [21] Bornot, S., Sifakis, J.: An Algebraic Framework for Urgency, Information and Computation, 163, 2000.
• [22] Bornot, S., Sifakis, J., Tripakis, S.: Modeling Urgency in Timed Systems, International Symposium: Compositionality - The Significant Difference, LNCS 1536, 1998.
• [23] Caspi, P., Benveniste, A.: Towards an Approximation Theory for Computerised Control, EMSOFT'02 (A. Sangiovanni-Vincentelli, J. Sifakis, Eds.), LNCS 2491, Grenoble, October 2002.
• [24] Chandy, K. M., Lamport, L.: Distributed Snapshots: Determining Global States of Distributed Systems, ACM Trans. Comput. Syst., 3(1), 1985, 63-75.
• [25] Chaochen, Z., Hoare, C. A. R., Ravn, A. P.: A Calculus of Durations., Inf. Process. Lett., 40(5), 1991, 269-276.
• [26] Chellas, B. F.: Modal Logic, an Introduction, Cambridge University Press, 1980.
• [27] Emerson, E. A., Halpern, J. Y.: "Sometimes" and "not never" revisited: On Branching versus Linear Time, 10th ACMSymposium on Principles of Programming Languages (POPL 83), 1983, Also published in Journal of ACM , 33:151-178.
• [28] Emerson, E. A., Mok, A. K., Sistla, A. P., Srinivasan, J.: Quantitative Temporal Reasoning, Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, LNCS 407, 1989.
• [29] Esterel Technologies: SCADE Suite, http://www.esterel-technologies.com/products/scade-suite/overview.html.
• [30] ETSI: ES 201 873 1, v2.2.1: "The Testing and Test Control Notation TTCN-3: Core Language ", 2002.
• [31] Fidge, C. J.: Logical Time in Distributed Computing Systems., IEEE Computer, 24(8), 1991, 28-33.
• [32] Glässer, U., Gotzhein, R., Prinz, A.: The Formal Semantics of SDL-2000: Status and Perspectives, Computer Networks, 42(3), 2003, 343-358.
• [33] Godefroid, P.: Using Partial Orders to Improve Automatic Verification Methods, Workshop on Computer-Aided Verification (CAV), Rutgers, LNCS 531, 1990.
• [34] Gurevich, Y.: Evolving Algebras 1993: Lipari Guide, in: Specification and Validation Methods (E. Börger, Ed.), Oxford University Press, 1995, 9-36.
• [35] Gurevich, Y., Huggins, J.: The Railroad Crossing Problem: An Experiment with Instantaneous Actions and Immediate Reactions, Proceedings of CSL'95 (Computer Science Logic), LNCS 1092, 1996.
• [36] Gurevich, Y., Schulte, W., Campbell, C., Grieskamp, W.: AsmL: The Abstract State Machine Language, Technical report, Version 2.0, Microsoft Research, Redmond, 2002.
• [37] Harel, E., Lichtenstein, O., Pnueli, A.: Explicit Clock Temporal Logic, 5th Symposium on Logic in Computer Science (LICS 90), IEEE, 1990.
• [38] Henzinger, T. A.: The Theory of Hybrid Automata., Conference on Logic in Computer Science, LICS, 1996.
• [39] Henzinger, T. A., Horowitz, B., Kirsch, C. M.: Giotto: A Time-Triggered Language for Embedded Programming., Embedded Software, 1st International Workshop, EMSOFT 2001, Tahoe, LNCS 2211, 2001.
• [40] Henzinger, T. A., Manna, Z., Pnueli, A.: What Good Are Digital Clocks?, Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, LNCS 623, 1992.
• [41] Henzinger, T. A., Nicollin, X., Sifakis, J., Yovine, S.: SymbolicModel Checking for Real-Time Systems, Inf. Comput., 111(2), 1994, 193-244.
• [42] Hirschfeld, Y., Rabinovich, A. M.: Logics for Real Time: Decidability and Complexity, Fundam. Inform., 62(1), 2004.
• [43] Ilogix: Rhapsody Development Environment, http://www.ilogix.com/rhapsody/rhapsody.cfm.
• [44] Ilogix: Statemate for Embedded Systems Design Software, http://www.ilogix.com/.
• [45] ISO/IEC: E-LOTOS (Enhanced LOTOS), ISO/IEC standard, 2001.
• [46] ITU-T: Recommendation Z.100. Specification and Description Language (SDL), Technical Report Z-100, International Telecommunication Union - Standardisation Sector, November 2000.
• [47] ITU-T: ITU-T Study Group 10: SDL Semantics, 2002, URL: http://rn.informatik.uni-kl.de/projects/sdl/.
• [48] Katoen, J.-P., Langerak, R., Latella, D., Brinksma, E.: On Specifying Real-Time Systems in a Causality-Based Setting., Formal Techniques in Real-Time and Fault-Tolerant Systems, 4th International Symposium, FTRTFT'96, Uppsala, LNCS 1135, 1996.
• [49] Kopetz, H., Grünsteidl, G.: TTP - A Time-Triggered Protocol for Fault-Tolerant Real-Time Systems., Symposium on Fault-Tolerant Computing, FTCS, Toulouse, IEEE, 1993.
• [50] Koymans, R.: Specifying Real-Time Properties withMetric Temporal Logic., Real-Time Systems, 2(4), 1990, 255-299.
• [51] Lamport, L.: The Temporal Logic of Actions, ACM Transactions on Programming Languages and Systems, 16(3), May 1994.
• [52] Lamport, L.: Real-Time Model Checking is Really Simple, CHARME 2005, Saarbruecken, LNCS, 2005.
• [53] MathWorks: MATLAB and Simulink for Technical Computing, http://www.mathworks.com/.
• [54] Nicollin, X., Sifakis, J.: An Overview and Synthesis on Timed Process Algebras., REX Workshop, LNCS 600, 1991.
• [55] Nielsen, M., Plotkin, G. D., Winskel, G.: Petri Nets, Event Structures and Domains, Part I., Theor. Comput. Sci., 13, 1981, 85-108.
• [56] Nunes, I., Fiadeiro, J. L., Turski, W. M.: Coordination Durative Actions., COORDINATION, LNCS 1282, 1997.
• [57] Nunes, I., Fiadeiro, J. L., Turski, W. M.: A Modal Logic of Durative Actions, Advances in Temporal Logic, Kluwer Academic Publishers, 2000.
• [58] Ouaknine, J., Worrell, J.: Revisiting Digitization, Robustness, and Decidability for Timed Automata., 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, IEEE Computer Society, 2003.
• [59] Peled, D.: All from One, One for All: On Model Checking Using Representatives., Computer Aided Verification, 5th International Conference, CAV '93, Elounda, Greece, LNCS 697, 1993.
• [60] Pnueli, A.: The Temporal Logic of Programs, 18th Symposium on Foundations of Computer Science (FOCS 77), IEEE, 1977, Revised version published in TCS, 13:45-60, 1981.
• [61] Prior, A. N.: Past, Present, Future, Oxford University Press, 1967.
• [62] Puri, A.: Dynamical Properties of Timed Automata., Formal Techniques in Real-Time and Fault-Tolerant Systems, 5th International Symposium, FTRTFT'98, Lyngby, LNCS 1486, 1998.
• [63] Rescher, N., Urquhart, A.: Temporal Logic, Springer Verlag, 1971.
• [64] Rust, H.: Hybrid Abstract State Machines: Using the Hyperreals for Describing Continuous Changes in a Discrete Notation, Abstract StateMachines - ASM2000, InternationalWorkshop on Abstract StateMachines, Monte Verita, Switzerland (Y. Gurevich, P. Kutter, M. Odersky, L. Thiele, Eds.), nr 87 in TIK-Report, Swiss Federal Institute of Technology (ETH) Zurich, March 2000.
• [65] Shields, M.: Concurrent Machines, Theoretical Computer Science, 28, 1985, 449-465.
• [66] Slissenko, A.: A Logic Framework for Verification of Timed Algorithms., Fundam. Inform., 62(1), 2004, 29-67.
• [67] Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001.
• [68] Trakhtenbrot, B. A.: Understanding Automata Theory in the Continuous Time Setting, Fundam. Inform., 62(1), 2004.
• [69] Tripakis, S.: Verifying Progress in Timed Systems., ARTS, LNCS 1601, 1999.
• [70] Tripakis, S., Yovine, S., Bouajjani, A.: Checking Timed Büchi Automata Emptiness Efficiently., Formal Methods in System Design, 26(3), 2005, 267-292.
• [71] Wang, J.: Timed Petri Nets: Theory and Application, Kluwer, 1998.
• [72] Winskel, G.: Events in Computation, Phd in Computer Science, University of Edinburgh, 1980.