Real-time specification patterns

ABSTRACT

Embedded systems are pervasive and frequently used for critical systems with time-dependent functionality. Dwyer et al have developed qualitative specification patterns to facilitate the specification of critical properties, such as those that must be satisfied by embedded systems. Thus far, no analogous repository has been compiled for real-time specification patterns. This paper makes two main contributions: First, based on an analysis of timing-based requirements of several industrial embedded system applications, we created real-time specification patterns in terms of three commonly used real-time temporal logics. Second, as a means to further facilitate the understanding of the meaning of a specification, we offer a structured English grammar that includes support for real-time properties. We illustrate the use of the real-time specification patterns in the context of property specifications of a real-world automotive embedded system.

REFERENCES

• 1: Luca Aceto , Patricia Bouyer , Augusto Burgueño , Kim G. Larsen, The power of reachability testing for timed automata, Theoretical Computer Science, v.300 n.1-3, p.411-475, 07 May 2003 [doi>10.1016/S0304-3975(02)00334-1]
• 2: Rajeev Alur, Techniques for automatic verification of real-time systems, Stanford University, Stanford, CA, 1992
• 3: Rajeev Alur , Thomas A. Henzinger, Logics and Models of Real Time: A Survey, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.74-106, June 03-07, 1991
• 4: Rajeev Alur , Thomas A. Henzinger, Real-time logics: complexity and expressiveness, Information and Computation, v.104 n.1, p.35-77, May 1993 [doi>10.1006/inco.1993.1025]
• 5: Rajeev Alur , Thomas A. Henzinger, A really temporal logic, Journal of the ACM (JACM), v.41 n.1, p.181-203, Jan. 1994 [doi>10.1145/174644.174651]
• 6: V. Ambriola , V. Gervasi, Processing natural language requirements, Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE), p.36, November 02-05, 1997
• 7: P. Bellini , R. Mattolini , P. Nesi, Temporal logics for real-time system specification, ACM Computing Surveys (CSUR), v.32 n.1, p.12-42, March 2000 [doi>10.1145/349194.349197]
• 8: D. Bošnački. Digitization of timed automata. In Proc. of the Fourth Int. Workshop on Formal Methods for Industrial Critical Systems FMICS '99, pages 283--302, Trento, Italy, 1999.
• 9: Marius Bozga , Conrado Daws , Oded Maler , Alfredo Olivero , Stavros Tripakis , Sergio Yovine, Kronos: A Model-Checking Tool for Real-Time Systems, Proceedings of the 10th International Conference on Computer Aided Verification, p.546-550, June 28-July 02, 1998
• 10: B. Bryant. Object-oriented natural language requirements specification. In Proc. of the 23rd Australasian Computer Science Conf., Canberra, Australia, 2000.
• 11: Marsha Chechik , Dimitrie O. Paun, Events in Property Patterns, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking, p.154-167, September 21-24, 1999
• 12: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 13: P. Clements, C. L. Heitmeyer, B. G. Labau, and A. T. Rose. MT: A toolset for specifying and analyzing real-time systems. In IEEE Real-Time Systems Symposium, December 1993.
• 14: Robert Darimont , Axel van Lamsweerde, Formal refinement patterns for goal-driven requirements elaboration, Proceedings of the 4th ACM SIGSOFT symposium on Foundations of software engineering, p.179-190, October 16-18, 1996, San Francisco, California, United States
• 15: Bruce Powel Douglass, Doing hard time: developing real-time systems with UML, objects, frameworks, and patterns, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 16: Doron Drusinsky, The Temporal Rover and the ATG Rover, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.323-330, August 30-September 01, 2000
• 17: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 18: A. Fantechi , S. Gnesi , G. Ristori , M. Carenini , M. Vanocchi , P. Moreschini, Assisting requirement formalization by means of natural language translation, Formal Methods in System Design, v.4 n.3, p.243-263, May 1994 [doi>10.1007/BF01384048]
• 19: S. Flake, W. Mueller, and J. Ruf. Structured English for model checking specifications. In Proc. of the GI-Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", Frankfurt, Germany, February 2000.
• 20: N. E. Fuchs and R. Schwitter. Attempto controlled English (ACE). In The First Int. Workshop on Controlled Language Applications (CLAW), Leuven, BE, March 1996.
• 21: Erich Gamma , Richard Helm , Ralph Johnson , John Vlissides, Design patterns: elements of reusable object-oriented software, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 22: Carlo Ghezzi , Richard A. Kemmerer, ASTRAL: An Assertion Language for Specifying Realtime Systems, Proceedings of the 3rd European Software Engineering Conference, p.122-146, October 21-24, 1991
• 23: 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]
• 24: C. L. Heitmeyer and R. Bharadwaj. Applying the SCR requirements method to the light control case study. Journal of Universal Computer Science, 6(7):650--678, 2000.
• 25: T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: A model checker for hybrid systems. Int. Journal on Software Tools for Technology Transfer, 1(1--2):110--122, 1997.
• 26: Thomas A. Henzinger , Zohar Manna , Amir Pnueli, What Good Are Digital Clocks?, Proceedings of the 19th International Colloquium on Automata, Languages and Programming, p.545-558, July 13-17, 1992
• 27: Alexander Holt , Ewan Klein, A semantically-derived subset of English for hardware verification, Proceedings of the 37th annual meeting of the Association for Computational Linguistics on Computational Linguistics, p.451-456, June 20-26, 1999, College Park, Maryland [doi>10.3115/1034678.1034747]
• 28: G. Holzmann. The Spin Model Checker, Primer and Reference Manual. Addison-Wesley, Reading, Massachusetts, 2004.
• 29: F Jahanian , A K Mok, Safety analysis of timing properties in real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.890-904, Sept. 1986
• 30: Sascha Konrad , Laura A. Campbell , Betty H. C. Cheng, Automated Analysis of Timing Information in UML Diagrams, Proceedings of the 19th IEEE international conference on Automated software engineering, p.350-353, September 20-24, 2004 [doi>10.1109/ASE.2004.14]
• 31: S. Konrad and B. H. C. Cheng. Real-time specification patterns. Technical Report MSU-CSE-04-37, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, September 2004.
• 32: S. Konrad and B. H. C. Cheng. Facilitating the derivation and instantiation of specification patterns. Technical Report MSU-CSE-05-4, Computer Science and Engineering, Michigan State University, East Lansing, Michigan, January 2005.
• 33: Sascha Konrad , Betty H. C. Cheng , Laura A. Campbell, Object Analysis Patterns for Embedded Systems, IEEE Transactions on Software Engineering, v.30 n.12, p.970-992, December 2004 [doi>10.1109/TSE.2004.102]
• 34: Ron Koymans, Specifying real-time properties with metric temporal logic, Real-Time Systems, v.2 n.4, p.255-299, Nov. 1990 [doi>10.1007/BF01995674]
• 35: Emmanuel Letier , Axel van Lamsweerde, Deriving operational software specifications from system goals, Proceedings of the 10th ACM SIGSOFT symposium on Foundations of software engineering, November 18-22, 2002, Charleston, South Carolina, USA [doi>10.1145/587051.587070]
• 36: Nancy A. Lynch , Frits W. Vaandrager, Forward and Backward Simulations for Timing-Based Systems, Proceedings of the Real-Time: Theory in Practice, REX Workshop, p.397-446, June 03-07, 1991
• 37: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 38: R. Mattolini. TILCO: A temporal logic for the specification of real-time systems. PhD thesis, 1996.
• 39: William E. McUmber , Betty H. C. Cheng, A general framework for formalizing UML with formal languages, Proceedings of the 23rd International Conference on Software Engineering, p.433-442, May 12-19, 2001, Toronto, Ontario, Canada
• 40: James Bret Michael , Vanessa L. Ong , Neil C. Rowe, Natural-Language Processing Support for Developing Policy-Governed Software Systems, Proceedings of the 39th International Conference and Exhibition on Technology of Object-Oriented Languages and Systems (TOOLS39), p.263, July 29-August 03, 2001
• 41: 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]
• 42: Rani Nelken , Nissim Francez, Automatic Translation of Natural Language System Specifications, Proceedings of the 8th International Conference on Computer Aided Verification, p.360-371, August 03, 1996
• 43: Kurt M. Olender , Leon J. Osterweil, Cecil: A Sequencing Constraint Language for Automatic Static Analysis Generation, IEEE Transactions on Software Engineering, v.16 n.3, p.268-280, March 1990 [doi>10.1109/32.48935]
• 44: J. Ostroff and W. Wonham. Modeling and verifying real-time embedded computer systems. In Proc. of the IEEE Real-Time Systems Symposium, pages 124--132, December 1987.
• 45: P. Pettersson and K. G. Larsen. Uppaal2k. Bulletin of the European Association for Theoretical Computer Science, 70:40--44, February 2000.
• 46: Y. S. Ramakrishna , P. M. Melliar-Smith , L. E. Moser , L. K. Dillon , G. Kutty, Interval logics and their decision procedures: part I: an interval logic, Theoretical Computer Science, v.166 n.1-2, p.1-47, Oct. 20, 1996 [doi>10.1016/0304-3975(95)00254-5]
• 47: Robert Bosch GmbH. Controller Area Network (CAN), 2005. http://www.can.bosch.com/.
• 48: M. A. A. Sanvido. Hardware-in-the-loop Simulation Framework. PhD thesis, Swiss Federal Institute of Technology, March 2002.
• 49: Rachel L. Smith , George S. Avrunin , Lori A. Clarke , Leon J. Osterweil, PROPEL: an approach supporting property elucidation, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581345]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
          Subjects: Methodologies (e.g., object-oriented, structured)

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

General Terms:
Verification

Keywords:
embedded systems, formal specification, patterns, real-time requirements