A temporal logic view of paradigm models

ABSTRACT

Software systems have evolved from monolithic programs to systems constructed from parallel, cooperative components, as can be currently found in object-oriented applications. Although powerful, these cooperative systems are also more difficult to verify.We show it is possible to automatically translate a PARADIGM specification to a Propositional Linear Temporal Logic based program. This has several interesting consequences: a) on one hand we allow a more declarative view of PARADIGM specifications, b) the resulting translation is an executable specification and c) as we show in this work it can also be useful on verifying correctness properties by automatic means. We think this will contribute to enhance the understanding, usability and further development of PARADIGM, and related methods like SOCCA, within both the Software Engineering and the Knowledge Engineering communities.

REFERENCES

• 1: Juan Carlos Augusto and Rodolfo Gómez. A Procedure to Translate Paradigm Specifications to Propositional Linear Temporal Logic and its Application to Verification. Technical report, Department of Electronics and Computer Science, University of Southampton, U.K., 2002, 40 pags. (http://www.ecs.soton.ac.uk/~jca/Par2PLTL.pdf).
• 2: Nikolaj S. Bjørner , Anca Browne , Michael A. Colón , Bernd Finkbeiner , Zohar Manna , Henny B. Sipma , Tomás E. Uribe, Verifying Temporal Properties of Reactive Systems: A STeP Tutorial, Formal Methods in System Design, v.16 n.3, p.227-270, June 2000 [doi>10.1023/A:1008700623084]
• 3: M. L. Cobo and J. C. Augusto. Logical Foundations and Implementation of an Extension of Temporal Prolog. The Journal of Computer Science and Technology (JCS&T), sponsored by ISTEC (Iberoamerican Science & Technology Education Consortium), 1(2):22-36, 1999.
• 4: Jürgen Ebert, Luuk Groenewegen, and Roger Süttenbach. A Formalization of SOCCA. Fachberichte Informatik 10-99, Universität Koblenz-Landau, Universität Koblenz-Landau, Institut für Informatik, Rheinau 1, D-56075 Koblenz, 1999.
• 5: Kousha Etessami, Stutter-Invariant Languages, omega-Automata, and Temporal Logic, Proceedings of the 11th International Conference on Computer Aided Verification, p.236-248, July 06-10, 1999
• 6: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 7: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 8: Zohar Manna , Amir Pnueli, The anchored version of the temporal framework, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.201-284, May 30-June 03, 1988
• 9: Amir Pnueli. Deduction is forever (invited talk). In Formal Methods'99, Toulouse, France, September, 1999.
• 10: Maarten van Steen , Luuk Groenewegen , Ger Oosting, Parallel Control Processes: Modular Parallelism and Communication, Intelligent Autonomous Systems, An International Conference, p.562-579, December 08-11, 1986
• 11: Sergio Yovine. Kronos: A Verification Tool for Real-Time Systems. Springer International Journal of Software Tools for Technology Transfer, 1997.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

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

  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
        I.2.11 Distributed Artificial Intelligence

Keywords:
paradigm, temporal logic, verification