Towards the compositional verification of real-time UML designs

ABSTRACT

Current techniques for the verification of software as e.g. model checking are limited when it comes to the verification of complex distributed embedded real-time systems. Our approach addresses this problem and in particular the state explosion problem for the software controlling mechatronic systems, as we provide a domain specific formal semantic definition for a subset of the UML 2.0 component model and an integrated sequence of design steps. These steps prescribe how to compose complex software systems from domain-specific patterns which model a particular part of the system behavior in a well-defined context. The correctness of these patterns can be verified individually because they have only simple communication behavior and have only a fixed number of participating roles. The composition of these patterns to describe the complete component behavior and the overall system behavior is prescribed by a rigorous syntactic definition which guarantees that the verification of component and system behavior can exploit the results of the verification of individual patterns.

REFERENCES

• 1: R. Alur, C. Courcoubetis, and D.L. Dill. Model Checking for Real-Time Systems. In IEEE Symposium on Logic in Computer Science (LICS), pages 414--425, Washington, D.C., 1990.
• 2: Maher Awad , Juha Kuusela , Jürgen Ziegler, Object-oriented technology for real-time systems: a practical approach using OMT and Fusion, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
• 3: Gerd Behrmann , Johan Bengtsson , Alexandre David , Kim Guldstrand Larsen , Paul Pettersson , Wang Yi, UPPAAL Implementation Secrets, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.3-22, September 09-12, 2002
• 4: Julian C. Bradfield , Juliana Küster Filipe , Perdita Stevens, Enriching OCL Using Observational Mu-Calculus, Proceedings of the 5th International Conference on Fundamental Approaches to Software Engineering, p.203-217, April 08-12, 2002
• 5: Sérgio Vale Aguiar Campos , Edmund M. Clarke , Marius Minea, The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems, Proceedings of the 9th International Conference on Computer Aided Verification, p.452-455, June 22-25, 1997
• 6: María Victoria Cengarle , Alexander Knapp, Towards OCL/RT, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.390-409, July 22-24, 2002
• 7: William Chan , Richard J. Anderson , Paul Beame , Steve Burns , Francesmary Modugno , David Notkin , Jon D. Reese, Model Checking Large Software Specifications, IEEE Transactions on Software Engineering, v.24 n.7, p.498-520, July 1998 [doi>10.1109/32.708566]
• 8: E. M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, January 2000.
• 9: Bruce Powel Douglass. Real-Time UML: Developing Efficient Objects for Embedded Systems. The Addison-Wesley Object Technology Series. Addison-Wesley, October 1999. Second Edition.
• 10: E. A. Emerson , A. K. Mok , A. P. Sistla , J. Srinivasan, Quantitative temporal reasoning, Real-Time Systems, v.4 n.4, p.331-352, Dec. 1992 [doi>10.1007/BF00355298]
• 11: Stephan Flake , Wolfgang Mueller, An OCL Extension for Real-Time Constraints, Object Modeling with the OCL, The Rationale behind the Object Constraint Language, p.150-171, January 2002
• 12: H. Giese and S. Burmester. Real-Time Statechart Semantics. Technical Report tr-ri-03-239, Computer Science Department, University of Paderborn, June 2003.
• 13: Holger Giese, Contract-Based Component System Design, Proceedings of the 33rd Hawaii International Conference on System Sciences-Volume 8, p.8051, January 04-07, 2000
• 14: Holger Giese. A formal calculus for the compositional pattern-based design of correct real-time systems. Technical Report tr-ri-03-240, Computer Science Department, University of Paderborn, July 2003.
• 15: Holger Giese, Stephan Flake, Wilhelm Schäfer, Matthias Tichy, Sven Burmester, and Daniela Schilling. Towards the compositional verification of real-time uml designs. Technical Report tr-ri-03-241, Computer Science Department, University of Paderborn, July 2003.
• 16: Hassan Gomaa, Designing Concurrent, Distributed, and Real-Time Applications with Uml, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 17: Hans J. Köhler , Ulrich Nickel , Jörg Niere , Albert Zündorf, Integrating UML diagrams for production control systems, Proceedings of the 22nd international conference on Software engineering, p.241-251, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337207]
• 18: Harry Li , Shriram Krishnamurthi , Kathi Fisler, Verifying cross-cutting features as open systems, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587066]
• 19: Gerald Lüttgen , Michael von der Beeck , Rance Cleaveland, A compositional approach to statecharts semantics, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.120-129, November 06-10, 2000, San Diego, California, United States
• 20: J. Misra and M. Chandy. Proofs of Networks of Processes. IEEE Transactions on Software Engineering, 7(4):417--426, 1981.
• 21: Object Management Group. UML Profile for Schedulability, Performance, and Time Specification. OMG Document ptc/02-03-02, September 2002. URL: http://cgi.omg.org/docs/ptc/02-03-02.pdf.
• 22: Object Management Group. UML Superstructure Submission V2.0. OMG Document ad/03-04-01, April 2003. URL: http://www.omg.org/cgi-bin/doc?ad/2003-04-01.
• 23: Jürgen Ruf. RAVEN: Real-Time Analyzing and Verification Environment. Journal on Universal Computer Science (J.UCS), Springer, 7(1):89--104, February 2001.
• 24: Jürgen Ruf , Thomas Kropf, Analyzing real-time systems, Proceedings of the conference on Design, automation and test in Europe, p.243-249, March 27-30, 2000, Paris, France [doi>10.1145/343647.343775]
• 25: Bran Selic , Garth Gullekson , Paul T. Ward, Real-time object-oriented modeling, John Wiley & Sons, Inc., New York, NY, 1994
• 26: Bran Selic and Jim Rumbaugh. Using UML for Modeling Complex Real-Time Systems. Techreport, ObjectTime Limited, 1998.
• 27: S. Yovine. Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer, 1:123--133, October 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Patterns (e.g., client/server, pipeline, blackboard); Domain-specific architectures

General Terms:
Design, Performance, Reliability, Verification

Keywords:
embedded systems, object constraint language (OCL), pattern, real-time, unified modelling language (UML)