Toward a formal model for component interfaces for real-time systems

ABSTRACT

We give a model of component interface for real-time component based systems. We extend the specification of a method with a time constraint which is a relation between the resource availability and the amount of time spent to perform the method. We define a contract to include method specification, and define a component as an implementation of a contract. This implementation may require services from other components with some assumptions about the schedule for the use of shared methods and resources with the presence of concurrency. Our model supports the separation between functional and non-functional requirements, and the formal compositional verification of component-based real-time systems.

REFERENCES

• 1: Zhou Chaochen , Anders P. Ravn , Michael R. Hansen, An Extended Duration Calculus for Hybrid Real-Time Systems, Hybrid Systems, p.36-59, January 1993
• 2: Dino Distefano , Joost-Pieter Katoen , Arend Rensink, On a temporal logic for object-based systems, Fourth International Conference on Formal methods for open object-based distributed systems IV, p.305-325, September 2000, Stanford, California, United States
• 3: Stephan Flake , Wolfgang Mueller, A UML Profile for Real-Time Constraints with the OCL, Proceedings of the 5th International Conference on The Unified Modeling Language, p.179-195, September 30-October 04, 2002
• 4: Dieter K. Hammer. Software Architectures and Component Technology (Editor: Mehmet Aksit), chapter Component-based Architecting for Distributed Real-time Systems. Kluwer, 2002.
• 5: C.A.R. Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall, 1998.
• 6: He Jifeng, Zhiming Liu, and Li Xiaoshan. Contract-Oriented Component Software Development. Technical Report 276, UNU-IIST, P.O.Box 3058, Macau, April 2003.
• 7: He Jifeng, Liu Zhiming, and Li Xiaoshan. Modelling Object-oriented Programming with Reference Type and Dynamic Binding. Technical Report 280, UNU-IIST, P.O.Box 3058, Macau, May 2003.
• 8: E.E. Roubtsova, J. van Katwijk, W.J.Toetenel, and R.C.M.de Rooij. Real-Time Systems: Specification of Properties in UML. In ASCI 2001 conference, pages pp.188--195, Het Heijderbos, Heijen, The Netherlands, May 30 - June 1 2001.
• 9: Shane Sendall , Alfred Strohmeier, Specifying Concurrent System Behavior and Timing Constraints Using OCL and UML, Proceedings of the 4th International Conference on The Unified Modeling Language, Modeling Languages, Concepts, and Tools, p.391-405, October 01-05, 2001
• 10: François Siewe , Dang Van Hung, Deriving Real-Time Programs from Duration Calculus Specifications, Proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.92-97, September 04-07, 2001
• 11: J. Sifakis, S. Tripakis, and S. Yovine. Building models of real-time systems from application software. In Special issue on modeling and design of embedded systems, volume 91(1) of Proceedings of the IEEE, pages 100--111, January 2003.
• 12: Hans Toetenel , Ella Roubtsova , Jan van Katwijk, A Timed Automata Semantics for Real-Time UML Specifications, Proceedings of the IEEE 2001 Symposia on Human Centric Computing Languages and Environments (HCC'01), p.88, September 05-07, 2001

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Theory

Keywords:
component-based systems, extended duration calculus, real-time constraints, unifying theory of programming