Validating real-time systems by history-checking TRIO specifications

ABSTRACT

We emphasize the importance of formal executable specifications in the development of real-time systems, as a means to assess the adequacy of the requirements before a costly development process takes place. TRIO is a first-order temporal logic language for executable specification of real-time systems that deals with time in a quantitative way by providing a metric to indicate distance in time between events and length of time intervals. We summarize the language and its model-parametric semantics. Then we present an algorithm to perform history checking, i.e., to check that a history of the system satisfies the specification. This algorithm can be used as a basis for an effective specification testing tool. The algorithm is described; an estimation of its complexity is provided; and the main functionalities of the tool are presented, together with sample test cases. Finally, we draw conclusions and indicate directions of future research.

REFERENCES

• 1: 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
• 2: Rajeev Alur , Thomas A. Henzinger, Real-time logics: complexity and expressiveness, Stanford University, Stanford, CA, 1990
• 3: ~ALUR, R. AND HENZrNGER, T.A. 1989. A really temporal logic. In Proceedings of the 30th ~Symposium on Foundations of Computer Science. IEEE Computer Science Press, Los Alamitos, ~Calif., 164-169.
• 4: ~ALUR, R., COUCORBERTIS, C., AND DILL, n. 1990. Model-checking for real-time systems. In the ~5th IEEE LICS 90. IEEE, New York, 414-425.
• 5: B Auernheimer , R A Kemmerer, RT-ASLAN: A specification language for real-time systems, IEEE Transactions on Software Engineering, v.12 n.9, p.879-889, Sept. 1986
• 6: ~BURCH, J., CLARKE, E., MILLAN, K. L. M., DILL, D., AND HWANO, H. 1990. Symbolic model ~checking: 10 A 20 states and beyond. In 5th Annual Symposium on Logic in Computer Science. ~IEEE, New York, 428-439.
• 7: 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]
• 8: A. Coen-Porisini , R. A. Kemmerer , D. Mandrioli, A Formal Framework for ASTRAL Intralevel Proof Obligations, IEEE Transactions on Software Engineering, v.20 n.8, p.548-561, August 1994 [doi>10.1109/32.310665]
• 9: ~COEN, A., MORZENTI, A., AND SCIUTO, D. 1991. Specification and verification of hardware ~systems using the temporal logic language TRIO. In Computer Hardware Description Lan- ~guages and their Application, D. Borrione and R. Waxman, Eds. North-Holland, Amsterdam, ~43-62.
• 10: ~CRIVELLI, E., MORZENTI, A., AND SAN PIETRO, P. 1990. Specification environments for real-time ~systems based on a logic language. Tech. annex to research contract 27/90, ENEL-CRA, ~December 1990. In Italian.
• 11: Miguel Felder , Angelo Morzenti, Validating real-time systems by history-checking TRIO specifications, Proceedings of the 14th international conference on Software engineering, p.199-211, May 11-15, 1992, Melbourne, Australia [doi>10.1145/143062.143115]
• 12: M. Felder , D. Mandrioli , A. Morzenti, Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models, IEEE Transactions on Software Engineering, v.20 n.2, p.127-141, February 1994 [doi>10.1109/32.265634]
• 13: 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
• 14: 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]
• 15: ~GHEZZI, C., MANDRIOLI, D., AND MORZENTI, A. 1989. TRIO, a logic language for executable ~specifications of real-time systems. In lOth French-Tunisian Seminar on Computer Science ~(Tunis, May), 322-349.
• 16: 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
• 17: KEMMERER, R.A. 1985. Testing formal specifications to detect design errors. IEEE Trans. ~Softw. Eng. 11, 1 (Jan.), 32-43.
• 18: ~KOYMANS, R. 1989. Specifying message passing and time critical systems with temporal logic. ~Ph.D. dissertation, Eindhoven Univ. of Technology, Eindhoven, The Netherlands.
• 19: Fred Kröger, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1987
• 20: ~MANDRIOLI, D., MORASCA, S., AND MORZENTI, A. 1992. Functional test case generation for ~real-time systems. In Proceedings of DCCA3: 3rd International Working Conference on De- ~pendable Computing for Crtt~cal Applications. IFIP, 13 26.
• 21: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 22: Angelo Morzenti , Pierluigi San Pietro, Object-oriented logical specification of time-critical systems, ACM Transactions on Software Engineering and Methodology (TOSEM), v.3 n.1, p.56-98, Jan. 1994 [doi>10.1145/174634.174636]
• 23: Angelo Morzenti , Dino Mandrioli , Carlo Ghezzi, A model parametric real-time logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.14 n.4, p.521-573, Oct. 1992 [doi>10.1145/133233.129397]
• 24: ~MORZEr~TI, A., RATTO, E., RONCATO, M., AND ZOCCOL~a~TE, L. 1989. TRIO: A logic formalism for ~the specification of real-time systems. In Euromicro Workshop on Real Time. IEEE, New York, ~26-30.
• 25: ~MORZENTI, h., PACI, M., AND VERONI, F. 1992b. Specification environments for real-time sys~ ~tems based on a logic language. Tech. annex to research contract 49/92, ENEL-CRA, Decem- ~ber 1992. In Italian.
• 26: Jonathan S. Ostroff, Temporal logic for real time systems, John Wiley & Sons, Inc., New York, NY, 1989
• 27: ~PNUELI, A. 1981. The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, ~45-60.
• 28: Franco P. Preparata , Michael I. Shamos, Computational geometry: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS
      Subjects: Real-time and embedded systems

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation
  D.4 OPERATING SYSTEMS
      D.4.7 Organization and Design
          Subjects: Real-time systems and embedded systems

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques; Mechanical verification

General Terms:
Languages, Verification

Keywords:
first-order logic, formal specifications, model-theoretic semantics, requirements validation