In: Lecture Notes in Computer Science : Formal Techniques for Networked and Distributed Systems - FORTE 2006, Volume 4229, 2006, pages 404-419. 2006. URL: http://dx.doi.org/10.1007/1188811629.
Abstract: The paper describes a transformational approach for the specification and formal verification of concurrent and real-time systems.At upper level, one system is specified using the timed process algebra RT-LOTOS. The output of the proposed transformation is a Time Petri net (TPN). The paper particularly shows how a TPN can be automatically constructed from an RT-LOTOS specification using a compositionally defined mapping. The proof of the translation consistency is sketched in the paper and developed in. The RT-LOTOS to TPN translation patterns formalized in the paper are being implemented. in a prototype tool. This enables reusing TPNs verification techniques and tools for the profit of RT-LOTOS.
Back to the Petri Nets Bibliography