Publication:
A formal library of set relations and its application to synchronous languages

Thumbnail Image
Files

Files

A formal library of set relations and its application to synchronous languages.pdf (372.26 KB)
View Statistics
Reference Managers
Mendeley
Indexers
Google Scholar CORE
QR Code
QR Code
Authors

Authors

Rocha, Camilo
Muñoz, César
Dowek, Gilles
Abstract (Spanish)
Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.
Abstract (English)
Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.
Extent
14 páginas.
URI: https://repositorio.escuelaing.edu.co/handle/001/1900
Collections

Collections

AD - CTG – Informática
References

M. AlTurki, J. Meseguer, Reduction semantics and formal analysis of Orc programs, Electr. Notes Theor. Comput. Sci. 200 (3) (2008) 25–41.

F. Baader, T. Nipkow, Term Rewriting and all that, Cambridge University Press, Cambridge, 1998.

J.-P. Banâtre, D.L. Métayer, The GAMMA model and its discipline of programming, Science of Computer Programming 15 (1) (1990) 55–77.

G. Berry, The foundations of Esterel, in: Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, Cambridge, MA, USA, 2000, pp. 425–454.

G. Berry, G. Boudol, The chemical abstract machine, Theoretical Computer Science 96 (1) (1992) 217–248.

P. Caspi, D. Pilaud, N. Halbwachs, J.A. Plaice, Lustre: a declarative language for real-time programming, in: POPL’87: Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages, ACM, New York, NY, USA, 1987, pp. 178–188.

M. Clavel, F. Durán, S. Eker, J. Meseguer, P. Lincoln, N. Martí-Oliet, C. Talcott, All About Maude — A High-Performance Logical Framework, 1st ed., in: LNCS, vol. 4350, Springer, 2007.

S. Dajani-Brown, D. Cofer, A. Bouali, Formal verification of an avionics sensor voter using SCADE, in: Y. Lakhnech, S. Yovine (Eds.), FORMATS/FTRTFT, in: Lecture Notes in Computer Science, vol. 3253, Springer, 2004, pp. 5–20.

R. De Simone, A. Ressouche, Compositional semantics of Esterel and verification by compositional reductions, Lecture Notes in Computer Science 818 (1994) 441–454.

N. Dershowitz, J.P. Jouannaud, Rewrite systems, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), The MIT Press, 1990, pp. 243–320.

G. Dowek, C. Muñoz, C. Păsăreanu, A formal analysis framework for PLEXIL, in: Proceedings of 3rd Workshop on Planning and Plan Execution for Real-World Systems, September 2007, pp. 45–51.

G. Dowek, C. Muñoz, C. Păsăreanu, A small-step semantics of PLEXIL, Technical Report 2008-11, National Institute of Aerospace, Hampton, VA, 2008.

G. Dowek, C. Muñoz, C. Rocha, Rewriting logic semantics of a plan execution language, CoRR abs/1002.2872, 2010.

T. Estlin, A. Jónsson, C. Păsăreanu, R. Simmons, K. Tso, V. Verna, Plan Execution Interchange Language (PLEXIL), Technical Memorandum TM-2006- 213483, NASA, 2006.

P.L. Guernic, T. Gautier, M.L. Borgne, C.L. Maire, Programming real-time applications with SIGNAL, Proceedings of the IEEE 79 (9) (1991) 1321–1336.

K. Harbusch, P. Poller, Structural translation with synchronous rewriting systems, Technical Report RT-94-01, Université Paris 7, Paris, France, 1994.

D. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming 8 (3) (1987) 231–274.

K. Heninger, Specifying software requirements for complex systems: new techniques and their application, IEEE Transactions on Software Engineering 6 (1) (1980) 2–13.

D. Lucanu, Strategy-based rewrite semantics for membrane systems preserves maximal concurrency of evolution rule actions, Electronic Notes in Theoretical Computer Science 237 (2009) 107–125.

G. Lüttgen, M. Beeck, R. Cleaveland, A compositional approach to statecharts semantics, in: ACM SIGSOFT 8th Intl. Symposium on Foundations of Software Engineering (FSE 2000), in: ACM Software Engineering Notes, vols. 25, 6, ACM Press, San Diego, California, November 2000, pp. 120–129.

G. Lüttgen, M. Mendler, Axiomatizing an algebra of step reactions for synchronous languages, in: L. Brim, P. Jancar, M. Kretínský, A. Kucera (Eds.), CONCUR, in: Lecture Notes in Computer Science, vol. 2421, Springer, 2002, pp. 386–401.

J. Meseguer, Conditional rewriting logic as a unified model of concurrency, Theoretical Computer Science 96 (1) (1992) 73–155.

J. Meseguer, Rewriting logic and Maude: a wide-spectrum semantic framework for object-based distributed systems, in: S.F. Smith, C.L. Talcott (Eds.), FMOODS, in: IFIP Conference Proceedings, vol. 177, Kluwer, 2000, p. 89.

J. Meseguer, G. Rosu, The rewriting logic semantics project, Theoretical Computer Science 373 (3) (2007) 213–237.

R. Owen, S. Giorgio, Synchronous models of language, in: Proceedings of the 34th annual meeting on Association for Computational Linguistics, Association for Computational Linguistics, Morristown, NJ, USA, 1996, pp. 116–123.

S. Owre, J. Rushby, N. Shankar, PVS: a prototype verification system, in: D. Kapur (Ed.), 11th International Conference on Automated Deduction (CADE), in: Lecture Notes in Artificial Intelligence, vol. 607, Springer-Verlag, Saratoga, NY, June 1992, pp. 748–752.

G.D. Plotkin, A structural approach to operational semantics, Journal of Logic and Algebraic Programming 60–61 (2004) 17–139.

P. Sampath, A.C. Rajeev, S. Ramesh, K.C. Shashidhar, Testing model-processing tools for embedded systems, in: IEEE Real-Time and Embedded Technology and Applications Symposium, IEEE Computer Society, 2007, pp. 203–214.

T. Serbanuta, G. Stefanescu, G. Rosu, Defining and executing P systems with structured data in k, in: D.W. Corne, P. Frisco, G. Paun, G. Rozenberg, A. Salomaa (Eds.), Workshop on Membrane Computing, in: Lecture Notes in Computer Science, vol. 5391, Springer, 2008, pp. 374–393.

O. Tardieu, A deterministic logical semantics for pure esterel, ACM Transactions on Programming Languages and Systems 29 (2) (2007) 8.

P. Viry, Equational rules for rewriting logic, Theoretical Computer Science 285 (2002) 487–517.