UML and RT-LOTOS: an integration for real-time system validation
作者： Pierre De Saqui-Sannes , Ludovic Apvrille , Christophe Lohr , Jean-Pierrre Courtiat , Patrick Senac
DOI:
关键词:
摘要: The paper presents a UML profile that overcomes the limitations of real-time solutions currently available on market. Associations between classes are given formal semantics. New temporal operators introduced; they include non deterministic delay and time-limited offering. models can be validated against logical timing constraints. profile’s semantics is through translation into language RT-LOTOS. latter supported by validation tool which generates reachability graphs from extended models. A coffee machine serves as example in paper. under evaluation satellite-based software reconfiguration system.
archives-ouvertes.fr参考文章(5)
L. Andriantsiferana, J.-P. Courtiat, R. C. Oliveira, L. Picci, An Experiment in using RT-LOTOS for the Formal Specification and Verification of a Distributed Scheduling Algorithm in a Nuclear Power Plant Monitoring System formal techniques for networked and distributed systems. pp. 433- 448 ,(1997) , 10.1007/978-0-387-35271-8_27
Issa Traoré, An Outline of PVS Semantics for UML Statecharts. Journal of Universal Computer Science. ,vol. 6, pp. 1088- 1108 ,(2000)
Bran Selic, Using UML for Modeling Complex Real-Time Systems languages compilers and tools for embedded systems. pp. 250- 260 ,(1998) , 10.1007/BFB0057795
J.-P. Courtiat, C.A.S. Santos, C. Lohr, B. Outtaj, Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique Computer Communications. ,vol. 23, pp. 1104- 1123 ,(2000) , 10.1016/S0140-3664(99)00240-6
Tommaso Bolognesi, Ed Brinksma, Introduction to the ISO specification language LOTOS Computer Networks and Isdn Systems. ,vol. 14, pp. 25- 59 ,(1987) , 10.1016/0169-7552(87)90085-7