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.
Supported in part by the NSF under grants HDR-9707076 and CCR-0098120, and by NASA under grant NAG 2-1440.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using Time Petri nets. IEEE Transactions on Software Engineering, 17(3):259–273, 1991.
J.E. Coolahan, Jr. and N. Roussopoulos. Timing requirements for time-driven systems using augmented Petri nets. IEEE Transactions on Software Engineering, 9(5):603–616, 1983.
J.P. Courtiat, C.A.S. Santos, C. Lohr, and B. Outtaj. Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Computer Communications, 23(12):1104–1123, 2000.
E.M. Clarke and J.M. Wing. Formal methods: state of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.
E.A. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 16. Elsevier Science Publisher B.V., 1990.
X. He and Y. Deng. A framework for developing and analyzing software architecture specifications in SAM. The Computer Journal, 45(1):111–128, 2002.
N.G. Leveson and J.L. Stolzy. Safety analysis using Petri nets. IEEE Transactions on Software Engineering, 13(3):386–397, 1987.
Z. Manna, A. Anuchitanukul, N. Bjørner, A. Browne, E. Chang, M. Colón, L. de Alaro, H. Devarajan, H. Sipma, and M. Uribe. STeP: the Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Department of Computer Science, Stanford University, June 1994.
P. Merlin and D.J. Faber. Recoverability of communication protocols. IEEE Transactions on Communications, COM-24(9):1036–1043, 1976.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
Z. Manna and A. Pnueli. Clocked transition systems. Technical Report STAN-CS-TR-96-1566, Computer Science Department, Stanford University, 1996.
T. Murata. Petri nets properties, analysis and applications. Proceedings of the IEEE, 77(4):27–60, 1989.
A. Pnueli. The temporal logic of programs. In 18th Ann. IEEE Symp. on Foundations of Computer Science, pages 46–57, 1977.
W3C Recommendation. Synchronized Multimedia Integration Language (SMIL) 1.0 Specification. http://www.w3.org/TR/REC-smil, 1998.
P.N.M. Sampaio and J.P. Courtiat. A formal approach for the presentation of interactive multimedia documents. In Proceedings Proceedings of the 7th ACM International Conference on Multimedia (Part 1), pages 435–438, 2000.
M. Trompedeller. A Classification of Petri Nets. http://www.daimi.dk/PetriNets/classification, 1995.
J. Wang, X. He, and Y. Deng. Introducing software architecture specification and analysis in SAM through an example. Information and Software Technology, 41:451–467, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yu, H., He, X., Deng, Y., Mo, L. (2002). Formal Analysis of Real-Time Systems with SAM. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_30
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive