In: Formal Methods and Software Engineering (ICFEM 2002), Proceedings of the 4th International Conference on Formal Engineering Methods, Shanghai, China, October 21-25, 2002, pages 275-286. Volume 2495 of Lecture Notes in Computer Science / C. George, H. Miao (Eds.) --- Springer Verlag, October 2002.
Abstract: The Software Architecture Model (SAM) is a general software architecture model based on a dual formalism combining Petri nets and temporal logic. This paper proposes a formal method for modeling and analyzing real-time systems with SAM. A high level Petri net and a linear time temporal logic are used as the theoretical basis for SAM. Behaviors of real-time systems are modeled by Petri nets, while their properties are specified by temporal logic. By translating Petri nets into clocked transition systems, we can apply the Stanford Temporal Prover to automating the analysis of real-time systems. A case study of interactive multimedia documents demonstrates our approach to modeling and analyzing real-time systems with SAM.
Keywords: Real-time system; SAM; Petri net; temporal logic; model; analysis.