Timed concurrent state machines

• Autorzy: Daszczuk W. B.

Warianty tytułu

PL

Współbieżne maszyny stanowe z czasem

• Języki publikacji: EN

Abstrakty

EN

Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.

PL

Współbieżne maszyny stanowe z czasem TCSM są aplikacją automatów czasowych Alura w środowisku koincydencyjnym współbieżnych maszyn czasowych CSM (w przeciwieństwie do środowisk przeplotowych). TCSM pasują do idei automatów testujących, które pozwalają wyspecyfikować zależności czasowe łatwiej niż poprzez formuły temporalne. Ponadto zdefiniowano sposób wyznaczania globalnej przestrzeni stanów w dziedzinie czasu (współbieżne maszyny stanowe regionów RCSM), co pozwala przechowywać badany system w postaci gotowej do weryfikacji i mnożyć go przez różne automaty testujące.

Słowa kluczowe

EN

formal methods; model checking; real time verification; Timed Automata

PL

metody formalne; weryfikacja modelowa; weryfikacja w czasie rzeczywistym; automat czasowy

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2007
• Tom: Vol. 8, Spec. Ed
• Strony: 23--36
• Opis fizyczny: Bibliogr. 14 poz., rys.

Twórcy

autor

Daszczuk W. B.

• Institute of Computer Science, Warsaw University of Technology, Warszawa, Poland,

Bibliografia

• [1] Alur R., Dill D. L.: A Theory of Timed Automata. Theoretical Computer Science, Vol. 126, 1994, p. 183-235
• [2] Alur R.: Timed Automata. in 11th International Conference on Computer-Aided Verification, LNCS 1633, Springer-Verlag, 1999, p. 8-22
• [3] Alur E., Courcoubetis C, Dill D. L.: Model-checking in dense real-time. Information and Computation, Vol 104, No. 1, 1993, p. 2-34
• [4] Daszczuk W. B.: Verification of Design Decisions in Communication Protocol by Evaluation of Temporal Logic Formulas. Institute of Computer Science, WUT, ICS Research Report No 22, 1998
• [5] Daszczuk W. B., Mieścicki J., Nowacki M., Wytrbowicz J.: System Level Specification and Yeńfication Using Concurrent State Machines and COSMA Environment. Proc. 8th International Conference on Mixed Design of Integrated Circuits and Systems, MDCDES 2001, June 21-23, Zakopane, Poland, 2001, p. 525-532
• [6] Daszczuk W. B., Grabski W., Mieścicki J., Wytrębowicz J.: System Modeling in the COSMA Environment. Proc. Euromicro Symposium on Digital Systems Design Architectures, Methods and Tools, September 4-6, Warsaw, Poland, IEEE Computer Society, Los Alamos, CA, 2001, p. 152-157
• [7] Daszczuk W. B.: Veńfication of Temporal Properties in Concurrent Systems,Ph.D. thesis, Warsaw University of Technology, 2003
• [8] Daszczuk W.B.: Timed Concurrent State Machines, Institute of Computer Science, WUT, ICS Research Report No 27, 2003
• [9] Mieścicki J.: Concurrent System of Communicating Machines, Institute of Computer Science, WUT, ICS Research Report No 35, 1992
• [10] Mieścicki J., Baszun M., Daszczuk W. B., Czejdo B.: Verification of Concurrent Engineering Software Using CSM Models, Proc. 2nd World Conf. on Integrated Design and Process Technology, Austin, Texas, USA, 1 4 Dec. 1996, 322-330
• [11] Mieścicki J., Czejdo B., Daszczuk W. B.: Model checking in the COSMA environ-ment as a support for the design of pipelined processing. Proc. European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyvaskyla, Finland, 24-28 July 2004
• [12] Mieścicki J., Czejdo B., Daszczuk W.B., Multi-phase model checking of a three-stage pipeline using the COSMA tool, Proc. European Congress on Computational Methods in Applied Sciences and Engineering ECCOMAS 2004, Jyvaskyla, Finland, 24-28 July 2004
• [13] Mieścicki J.: Verification of UML State Diagrams Using Concurrent State Machines, IFIP Working Conference on Software Engineering Techniques SET'2006, October 17-20 2006, Warsaw, Poland
• [14] Zhang Z.: An Approach to Hierarchy Model Checking via Evaluating CTL Hier-archically. Proc. of the 4th Asian Test Symposium, ATS'95, IEEE 1995, 45-49