A formal design notation for real-time systems

ABSTRACT

The development of real-time systems is based on a variety of different methods and notations. Despite the purported benefits of formal methods, informal techniques still play a predominant role in current industrial practice. Formal and informal methods have been combined in various ways to smoothly introduce formal methods in industrial practice. The combination of real-time structured analysis (SA-RT) with Petri nets is among the most popular approaches, but has been applied only to requirements specifications. This paper extends SA-RT to specifications of the detailed design of embedded real-time systems, and combines the proposed notation with Petri nets.

REFERENCES

• 1: ALUR, R., COURCOUBETIS, C., AND DILL, D. 1990. Model Checking for Real-Time Systems, in Proceedings of the IEEE 5th Annual Symposium on Logic in Computer Science.
• 2: Luciano Baresi , Alessandro Orso , Mauro Pezzè, Introducing formal specification methods in industrial practice, Proceedings of the 19th international conference on Software engineering, p.56-66, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253241]
• 3: L. Baresi , M. Pezzè, On formalizing UML with high-level petri nets, Concurrent object-oriented programming and petri nets: advances in petri nets, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 4: Augusto Burgueño , Vlad Rusu, Task-System Analysis Using Slope-Parametric Hybrid Automata, Proceedings of the Third International Euro-Par Conference on Parallel Processing, p.1262-1273, August 26-29, 1997
• 5: A. Burns , A. J. Wellings, HRT-HOOD: a structured design method for hard real-time systems, Real-Time Systems, v.6 n.1, p.73-114, Jan. 1994 [doi>10.1007/BF01245300]
• 6: S.-C. Cheng , J.-A. Stankovic , K. Ramamritham, Scheduling algorithms for hard real-time systems: a brief survey, Tutorial: hard real-time systems, IEEE Computer Society Press, Los Alamitos, CA, 1989
• 7: James C. Corbett, Timing Analysis of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.22 n.7, p.461-483, July 1996 [doi>10.1109/32.538604]
• 8: Bruce Powel Douglass, Real-time UML (2nd ed.): developing efficient objects for embedded systems, Addison-Wesley Longman Ltd., Essex, UK, 2000
• 9: S. Duri , U. Buy , R. Devarapalli , S. M. Shatz, Using state space reduction methods for deadlock analysis in Ada tasking, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.51-60, June 28-30, 1993, Cambridge, Massachusetts, United States
• 10: ELMSTROM, R., LINTULAMPI, R., AND PEZZE, M. 1993. Giving Semantics to SA/RT by Means of High- Level Timed Petri Nets. J. Real-Time Syst. (May) 5, 2/3, 249-272.
• 11: Miguel Felder , Carlo Ghezzi , Mauro Pezzè, Analyzing refinements of state based specifications: the case of TB nets, Proceedings of the 1993 ACM SIGSOFT international symposium on Software testing and analysis, p.28-39, June 28-30, 1993, Cambridge, Massachusetts, United States
• 12: FELDER, M. AND PEZZE, M. 1997. RTD: a design notation for Structured Analysis Real-Time, in Proceedings of the KIT125 Workshop on Formal Methods for the Design of Real-Time Systems, Como (Sept.).
• 13: Robert B. France, Semantically Extended Dataflow Diagrams: A Formal Specification Tool, IEEE Transactions on Software Engineering, v.18 n.4, p.329-346, April 1992 [doi>10.1109/32.129221]
• 14: Robert B. France , María M. Larrondo-Petrie, From structured analysis to formal specifications: state of the theory, Proceedings of the 22nd annual ACM computer science conference on Scaling up : meeting the challenge of complexity in real-world computing applications: meeting the challenge of complexity in real-world computing applications, p.249-256, March 08-10, 1994, Phoenix, Arizona, United States [doi>10.1145/197530.197634]
• 15: M. D. Fraser , K. Kumar , V. K. Vaishnavi, Informal and Formal Requirements Specification Languages: Bridging the Gap, IEEE Transactions on Software Engineering, v.17 n.5, p.454-466, May 1991 [doi>10.1109/32.90448]
• 16: FREDETTE, A. N. AND CLEAVELAND, R. 1993. RTSL: A Formal Language for Real-Time Schedulability Analysis, Proceedings of the Real-Time Systems Symposium, Durham, NC(Dec.), Computer Society Press, 274-283.
• 17: Carlo Ghezzi , Mehdi Jazayeri , Dino Mandrioli, Fundamentals of software engineering, Prentice-Hall, Inc., Upper Saddle River, NJ, 1991
• 18: Carlo Ghezzi , Dino Mandrioli , Sandro Morasca , Mauro Pezzè, A Unified High-Level Petri Net Formalism for Time-Critical Systems, IEEE Transactions on Software Engineering, v.17 n.2, p.160-172, February 1991 [doi>10.1109/32.67597]
• 19: C. Ghezzi , D. Mandrioli , A. Morzenti, TRIO: A logic language for executable specifications of real-time systems, Journal of Systems and Software, v.12 n.2, p.107-123, May 1990 [doi>10.1016/0164-1212(90)90074-V]
• 20: Carlo Ghezzi , Sandro Morasca , Mauro Pezzè, Validating timing requirements for time basic net specifications, Journal of Systems and Software, v.27 n.2, p.97-117, Nov. 1994 [doi>10.1016/0164-1212(94)90024-8]
• 21: Hassan Gomaa, Software Design Methods for Concurrent and Real-Time Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1993
• 22: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 23: Derek J. Hatley , Imtiaz A. Pirbhai, Strategies for real-time system specification, Dorset House Publishing Co., Inc., New York, NY, 1987
• 24: Catherine E. Houstis, Module Allocation of Real-Time Applications to Distributed Systems, IEEE Transactions on Software Engineering, v.16 n.7, p.699-709, July 1990 [doi>10.1109/32.56096]
• 25: IEEE 1993. Real-Time Extensions to POSIX, IEEE Standard P1003.1b, IEEE Press (March).
• 26: M. A Jackson, System development (Prentice-Hall International series in computer science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1983
• 27: JENSEN, K. 1996. Coloured Petri Nets. Monographs in Theoretical Computer Science, second edition, Springer-Verlag, Berlin.
• 28: Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
• 29: Klaus Kronlöf, Method integration: concepts and case studies, John Wiley & Sons, Inc., New York, NY, 1993
• 30: Leo Yuhsiang Liu , R. K. Shyamasundar, Static Analysis of Real-Time Distributed Systems, IEEE Transactions on Software Engineering, v.16 n.4, p.373-388, April 1990 [doi>10.1109/32.54290]
• 31: L. E. Moser , Y. S. Ramakrishna , G. Kutty , P. M. Melliar-Smith , L. K. Dillon, A graphical environment for the design of concurrent real-time systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.6 n.1, p.31-79, Jan. 1997 [doi>10.1145/237432.237438]
• 32: Nimal Nissanke, Realtime systems, Prentice-Hall, Inc., Upper Saddle River, NJ, 1997
• 33: Michael A. Palis , Jing-Chiou Liou , David S. L. Wei, Task Clustering and Scheduling for Distributed Memory Parallel Architectures, IEEE Transactions on Parallel and Distributed Systems, v.7 n.1, p.46-55, January 1996 [doi>10.1109/71.481597]
• 34: PEZZE, M. AND GHEZZI, C. 1992. Cabernet: an Environment for the Specification and Verification of Real-Time Systems, Proceeding of DECUS Europe Symposium, Cannes (France, Sept.).
• 35: G. Richter , B. Maffeo, Toward a Rigorous Interpretation of ESML-Extended Systems Modeling Language, IEEE Transactions on Software Engineering, v.19 n.2, p.165-180, February 1993 [doi>10.1109/32.214833]
• 36: John A. StankovicThis work was done while the , Marco Spuri , Marco Di Natale , Giorgio C. Buttazzo, Implications of Classical Scheduling Results for Real-Time Systems, Computer, v.28 n.6, p.16-25, June 1995 [doi>10.1109/2.386982]
• 37: Antti Valmari, A Stubborn Attack On State Explosion, Proceedings of the 2nd International Workshop on Computer Aided Verification, p.156-165, June 18-21, 1990
• 38: Enoch Y. Wang , Heather A. Richter , Betty H. C. Cheng, Formalizing and integrating the dynamic model within OMT, Proceedings of the 19th international conference on Software engineering, p.45-55, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253239]
• 39: Paul T. Ward , Stephen J. Mellor, Structured Development for Real-Time Systems, Prentice Hall Professional Technical Reference, 1991
• 40: WING, J. M. AND ZAREMSKI, A. M. 1991. Two Ways to Integrate Formal Specifications in Practice, In Proceedings of Formal Methods Europe.
• 41: Wei Jen Yeh , Michal Young, Compositional reachability analysis using process algebra, Proceedings of the symposium on Testing, analysis, and verification, p.49-59, October 08-10, 1991, Victoria, British Columbia, Canada [doi>10.1145/120807.120812]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Structured programming**
      D.2.3 Coding Tools and Techniques
          Subjects: Structured programming

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

General Terms:
Design

Keywords:
Formal design specification, design of real time systems, formal analysis of design specification, structured design