Formal Specification and Verification of Real-Time Systems using Graph Grammars

Springer Science and Business Media LLC - 2007
Leonardo Michelon1, Sérgio Ely Valadão Gigante de Andrade Costa1,2, Leila Ribeiro1
1Instituto de Informática, Universidade Federal do Rio Grande do Sul, Porto Alegre, Brazil
2Departamento de Informática, Universidade Federal de Pelotas, Pelotas, BRAZIL

Tóm tắt

Abstract The importance of real-time systems has enormously increased in the last decade. Application areas that typically need real-time models include railroad systems, intelligent vehicle highway systems, avionics, multimedia and telephony. To assure that such systems are correct, additionally to prove that they provide the required functionality, time constraints must be satisfied. There are already formal specification methods for real-time systems, but most of them are difficult to use by software developers, that are usually not very familiar with mathematical notation but rather specify systems using the objectoriented paradigm. In this paper we propose a formal approach to specify and analyze real-time systems that has an object-oriented flavor. This approach is based on Object-Based Graph Grammars (OBGGs), a formal description technique suitable for the specification of asynchronous distributed systems, and intuitive even for nontheoreticians. We extend OBGGs to enable explicit modeling of time constraints, and define the semantics of the specifications via transition systems. Finally, we translate timed OBGGs to Timed Automata, a formal notation that is wide spread in the area of real-time systems modeling and allows the automatic verification of properties.

Từ khóa


Tài liệu tham khảo

R. Alur and D. L. Dill. A theory of timed automata.Theoretical Computer Science, 126(2):183–235, 1994.

J. Baeten and C. Middelburg.Process algebra with timing: Real time and discrete time, chapter 10, pages 627–684. Elsevier, 2001.

G. Behrmann, A. David, and K. G. Larsen. Tutorial on UPPAAL. InFormal Methods for the Design of Real-Time Systems, volume 3185 of LNCS, pages 200–236. Springer, 2004.

J. Bengtsson and W. Yi. Timed automata: Semantics, algorithms and tools. InLecture Notes on Concurrency and Petri Nets, volume 3098 of LNCS, pages 87-124. Springer, 2004.

B. Berthomieu and M. Diaz. Modeling and verification of time dependent systems using time petri nets.IEEE Trans. Softw. Eng., 17(3):259–273, 1991.

H. Bowman and J. Derrick. Extending lotos with time: A true concurrency perspective. InAMAST Workshop on Real-Time Systems, Concurrent and Distributed Software, volume 1231 of LNCS, pages 382–399. Springer, 1997.

E. M. Clarke and J. M. Wing. Formal methods: state of the art and future directions.ACM Computing Surveys, 28(4):626–643, 1996.

A. Corradini, U. Montanari, and F. Rossi. Graph processes.Fundamenta Informaticae, 26(3/4):241–265, 1996.

K. Diethers and M. Huhn. Vooduu: Verification of object-oriented designs using uppaal. InTools and Algorithms for the Construction and Analysis of Systems, volume 2988 of LNCS, pages 139–143. Springer, 2004.

F. L. Dotti, L. Foss, L. Ribeiro, and O. M. Santos. Verification of distributed object-based systems. In6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems, volume 2884 of LNCS, pages 261–275. Springer, 2003.

F. L. Dotti and L. Ribeiro. Specification of mobile code systems using graph grammars. InFormal Methods for Open Object-Based Distributed Systems, pages 45–64. Kluwer, 2000.

L. M. Duarte, F. L. Dotti, B. Copstein, and L. Ribeiro. Simulation of mobile applications. InProc. of Communication Networks and Distributed Systems Modeling and Simulation Conference, volume 1, pages 1–15, 2002.

H. Ehrig, H.-J. Kreowski, U. Montanari, and G. Rozenberg, editors.Handbook of Graph Grammars and Computing by Graph Transformations, Volume 3: Concurrency, Parallelism and Distribution. World Scientific, 1999.

H. Ehrig and B. Mahr.Fundamentals of Algebraic Specification: Equations and Initial Algebra Semantics, volume 6 of EATCSMonographs on Theoretical Computer Science. Springer, 1985.

A. P. L. Ferreira.Object-Oriented Graph Grammars. PhD thesis, Universidade Federal do Rio Grande do Sul, 2005.

S. Graf, I. Ober, and I. Ober. A real-time profile for uml.International Journal on Software Tools for Technology Transfer, 8(2):113–127, 2006.

A. Haxthausen and J. Peleska. Formal development and verification of a distributed railroad control system.IEEE Transactions on Software Engineering, 26(8):687–701, August 2000.

A. Knapp, S. Merz, and C. Rauh. Model checking — timed uml state machines and collaborations. InProceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 395–416. Springer, 2002.

S. Konrad, L. A. Campbell, and B. H. C. Cheng. Automated analysis of timing information in uml diagrams. InProceedings of the 19th IEEE international conference on Automated software engineering, pages 350–353. IEEE Computer Society, 2004.

L. Lavazza, G. Quaroni, and M. Venturelli. Combining uml and formal notations for modelling real-time systems.SIGSOFT Softw. Eng. Notes, 26(5):196–206, 2001.

I. Lee, P. Brémond-Grégoire, and R. Gerber. A process algebraic approach to the specification and analysis of resource-bound real-time systems.Proc. of the IEEE, 82(1):158–171, 1994.

I. Ober, S. Graf, and I. Ober. Validation of uml models via a mapping to communicating extended timed automata. In SPIN, volume 2989 ofLNCS, pages 127–145. Springer, 2004.

L. Ribeiro, F. Dotti, and R. Bardohl. A formal framework for the development of concurrent object-based systems. InFormal Methods in Software and Systems Modeling, volume 3393 of LNCS, pages 385–401. Springer, 2005.

L. Ribeiro, F. L. Dotti, O. Santos, and F. Pasini. Verifying object-based graph grammars: An assumeguarantee approach.Software and Systems Modeling, 6(3):289–311, Sept. 2006.

G. Rozenberg, editor.Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations. World Scientific, 1997.

J. A. Stankovic. A serious problem for nextgeneration systems.IEEE Computer, 21(10):10–19, 1988.

J. A. Stankovic et al. Strategic directions in real-time and embedded systems.ACM Computing Surveys, 28(4):751–763, 1996.

B. Walter. Timed petri-nets for modelling and alalyzing protocols with real-time characteristics. InProtocol Specification, Testing, and Verification, pages 149–159. North-Holand, 1983.

Thông tin
Thông tin xuất bản

Springer Science and Business Media LLC

Thông tin tác giả