Verifying RTECTL properties of a train controller systems

• Autorzy: Woźna-Szcześniak B. , Zbrzezny A. , Zbrzezny Andrzej
• Języki publikacji: EN

Abstrakty

EN

In the paper we deal with a classic concurrency problem - a faulty train controller system (FTC). In particular, we formalize it by means of finite automata, and consider several properties of the problem, which can be expressed as formulae of a soft real-time branching time temporal logic, called RTECTL. Further, we verify the RTECTL properties of FTC by means of SAT-based bounded model checking (BMC) method, and present the performance evaluation of the BMC method with respect to the considered problem. The performance evaluation is given by means of the running time and the memory used.

Słowa kluczowe

EN

RTECTL; train controller systems; BMC method

PL

system kontrolera pociągu; metoda BMC

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2011
• Tom: Vol. 16
• Strony: 153--162
• Opis fizyczny: Bibliogr. 11 poz., rys., tab.

Twórcy

autor

Woźna-Szcześniak B.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny Andrzej

• Institute of Mathematics and Computer Science Jan Długosz University in Częstochowa al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• 1. R. Bryant. Binary Decision Diagrams and beyond: Enabling technologies for formal verification. In: Proceedings of the International Conference on Computer-Aided Design (ICCAD’95), pp. 236-243, 1995.
• 2. E. Clarke, A. Biere, R. Raimi, Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1), 7-34, 2001.
• 3. E.M. Clarke, O. Grumberg, D.A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• 4. D. Dams, O. Grumberg, R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In: Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi. Elsevier, 1994.
• 5. E.A. Emerson, A.K. Mok., A.P. Sistla, J. Srinivasan. Quantitative temporal reasoning. In: Proceedings of the 2nd International Workshop on Computer Aided Verification, pp. 136-145, Springer, London, 1991.
• 6. E.A. Emerson and A.P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9, 105-131, 1995.
• 7. W. van der Hoek, M. Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica, 75(1), 125-157, 2003.
• 8. K.L. McMillan, Applying SAT methods in unbounded symbolic model checking. In: Proc. of the 14th Int. Conf. on Computer Aided Verification, vol. 2404 of LNCS, pp. 250-264, Springer, London, 2002.
• 9. W. Penczek, B. Woźna, A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2), 135-156, 2002.
• 10. P. Wolper, P. Godefroid. Partial order methods for temporal verification. In: Proceedings of the 4th International Conference on Concurrency Theory, vol. 715 of LNCS, pp. 233-246, Springer, London, 1993.
• 11. B. Woźna-Szcześniak. Bounded model checking for the existential part of Real-Time CTL and knowledge. In Pre-Proceedings of CEE-SET’09, pp. 178-191, AGH Kraków, Poland, 2009.