research-article

The refinement calculus of reactive systems

Authors:

Viorel Preoteasa,

Iulia Dragomir,

Stavros TripakisAuthors Info & Claims

Volume 285, Issue PB

https://doi.org/10.1016/j.ic.2021.104819

Published: 01 May 2022 Publication History

Abstract

The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which can describe atomic components as symbolic transition systems or QLTL formulas, and composite components formed using three primitive composition operators: serial, parallel, and feedback. The semantics of the language is given in terms of monotonic property transformers, an extension of monotonic predicate transformers to reactive systems. RCRS can specify both safety and liveness properties. It can also model input-output systems which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS comes with a publicly available implementation which includes a complete formalization of the RCRS theory in the Isabelle proof assistant.

References

[1]

M. Abadi, L. Lamport, Conjoining specifications, ACM Trans. Program. Lang. Syst. 17 (3) (1995) 507–535.

[2]

E. Ábrahám-Mumm, M. Steffen, U. Hannemann, Verification of hybrid systems: formalization and proof rules in PVS, in: 7th Intl. Conf. Engineering of Complex Computer Systems, ICECCS 2001, 2001, pp. 48–57.

[3]

J.-R. Abrial, Modeling in Event-B: System and Software Engineering, 1st edition, Cambridge University Press, New York, NY, USA, 2010.

[4]

B. Alpern, F.B. Schneider, Defining liveness, Inf. Process. Lett. 21 (4) (1985) 181–185.

[5]

R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, S. Yovine, The algorithmic analysis of hybrid systems, Theor. Comput. Sci. 138 (1995) 3–34.

[6]

R. Alur, T. Henzinger, Reactive modules, Form. Methods Syst. Des. 15 (1999) 7–48.

[7]

R. Alur, T. Henzinger, O. Kupferman, M. Vardi, Alternating refinement relations, in: CONCUR'98, in: LNCS, vol. 1466, Springer, 1998.

[8]

A. Armstrong, V. Gomes, G. Struth, Building program construction and verification tools from algebraic principles, Form. Asp. Comput. 28 (2) (2016).

[9]

R.D. Arthan, P. Caseley, C. O'Halloran, A. Smith, ClawZ: control laws in Z, in: 3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000, York, England, UK, September 4–7, 2000, Proceedings, 2000, pp. 169–176.

[10]

R.J. Back, Correctness Preserving Program Refinements: Proof Theory and Applications, Mathematical Centre Tracts, vol. 131, Mathematisch Centrum, Amsterdam, 1980.

[11]

R.-J. Back, M. Butler, Exploring Summation and Product Operators in the Refinement Calculus, Springer, Berlin, Heidelberg, 1995, pp. 128–158.

[12]

R.-J. Back, J. von Wright, Refinement Calculus: A Systematic Introduction, Springer, 1998.

Digital Library

[13]

R.-J. Back, J. Wright, Trace refinement of action systems, in: B. Jonsson, J. Parrow (Eds.), CONCUR '94: Concurrency Theory, in: Lecture Notes in Computer Science, vol. 836, Springer, Berlin, Heidelberg, 1994, pp. 367–384.

[14]

R.-J. Back, Q. Xu, Refinement of fair action systems, Acta Inform. 35 (2) (1998) 131–165.

[15]

A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T.A. Henzinger, K.G. Larsen, Contracts for system design, Found. Trends Electron. Des. Autom. 12 (2–3) (2018) 124–400.

[16]

P. Boström, Contract-based verification of Simulink models, in: S. Qin, Z. Qiu (Eds.), Formal Methods and Software Engineering, in: Lecture Notes in Computer Science, vol. 6991, Springer, Berlin, Heidelberg, 2011, pp. 291–306.

[17]

R.J. Boulton, A. Gordon, M.J.C. Gordon, J. Harrison, J. Herbert, J.V. Tassel, Experience with embedding hardware description languages in HOL, in: IFIP TC10/WG 10.2 Intl. Conf. on Theorem Provers in Circuit Design, North-Holland Publishing Co., 1992, pp. 129–156.

[18]

M. Broy, K. Stølen, Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement, Springer, 2001.

Digital Library

[19]

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, S. Tonetta, The nuxmv symbolic model checker, in: A. Biere, R. Bloem (Eds.), Computer Aided Verification: 26th International Conference, CAV 2014, Springer, Cham, 2014, pp. 334–342.

[20]

A.L.C. Cavalcanti, A. Mota, J.C.P. Woodcock, Simulink timed models for program verification, in: Z. Liu, J.C.P. Woodcock, H. Zhu (Eds.), Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, in: Lecture Notes in Computer Science, vol. 8051, Springer, 2013, pp. 82–99.

[21]

A. Chakrabarti, L. de Alfaro, T. Henzinger, F. Mang, Synchronous and bidirectional component interfaces, in: CAV, in: LNCS, vol. 2404, Springer, 2002, pp. 414–427.

[22]

C. Chen, J.S. Dong, J. Sun, A formal framework for modeling and validating Simulink diagrams, Form. Asp. Comput. 21 (5) (2009) 451–483.

[23]

B. Courcelle, A representation of graphs by algebraic expressions and its use for graph rewriting systems, in: H. Ehrig, M. Nagl, G. Rozenberg, A. Rosenfeld (Eds.), Graph-Grammars and Their Application to Computer Science, 3rd International Workshop, in: Lecture Notes in Computer Science, vol. 291, Warrenton, Virginia, USA, December 2–6, 1986, Springer, 1986, pp. 112–132.

[24]

P. Cousot, R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, in: 4th ACM Symp. POPL, 1977.

[25]

L. de Alfaro, T. Henzinger, Interface automata, in: Foundations of Software Engineering, FSE, ACM Press, 2001.

[26]

L. de Alfaro, T. Henzinger, Interface theories for component-based design, in: EMSOFT'01, in: LNCS, vol. 2211, Springer, 2001.

[27]

W. de Roever, H. Langmaack, A.E. Pnueli, Compositionality: The Significant Difference, LNCS, Springer, 1998.

[28]

W.-P. de Roever, F. de Boer, U. Hanneman, J. Hooman, Y. Lakhnech, M. Poel, J. Zwiers, Concurrency Verification: Introduction to Compositional and Non-compositional Methods, Cambridge University Press, 2012.

[29]

K. Dhara, G. Leavens, Forcing behavioral subtyping through specification inheritance, in: ICSE'96: 18th Intl. Conf. on Software Engineering, IEEE Computer Society, 1996, pp. 258–267.

[30]

E. Dijkstra, Notes on structured programming, in: O. Dahl, E. Dijkstra, C. Hoare (Eds.), Structured Programming, Academic Press, London, UK, 1972, pp. 1–82.

[31]

E. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM 18 (8) (1975) 453–457.

Digital Library

[32]

D. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits, MIT Press, Cambridge, MA, USA, 1987.

[33]

L. Doyen, T. Henzinger, B. Jobstmann, T. Petrov, Interface theories with component reuse, in: 8th ACM & IEEE International Conference on Embedded Software, EMSOFT, 2008, pp. 79–88.

[34]

I. Dragomir, V. Preoteasa, S. Tripakis, Compositional semantics and analysis of hierarchical block diagrams, in: SPIN, Springer, 2016, pp. 38–56.

[35]

I. Dragomir, V. Preoteasa, S. Tripakis, The refinement calculus of reactive systems toolset. CoRR, abs/1710.08195, 2017.

[36]

I. Dragomir, V. Preoteasa, S. Tripakis, The refinement calculus of reactive systems toolset, in: TACAS, 2018.

[37]

I. Dragomir, V. Preoteasa, S. Tripakis, The refinement calculus of reactive systems toolset, Int. J. Softw. Tools Technol. Transf. (2020) 1–20.

[38]

R. Floyd, Assigning meanings to programs, In. Proc. Symp. on Appl. Math., vol. 19, American Mathematical Society, 1967, pp. 19–32.

[39]

T. Freeman, F. Pfenning, Refinement types for ML, SIGPLAN Not. 26 (6) (May 1991) 268–277.

[40]

P. Fritzson, Principles of Object-Oriented Modeling and Simulation with Modelica 3.3: A Cyber-Physical Approach, 2 edition, Wiley, 2014.

[41]

N. Fulton, S. Mitsch, J.-D. Quesel, M. Völp, A. Platzer, KeYmaera X: an axiomatic tactical theorem prover for hybrid systems, in: A.P. Felty, A. Middeldorp (Eds.), CADE, in: LNCS, vol. 9195, Springer, 2015, pp. 527–538.

[42]

O. Grumberg, D. Long, Model checking and modular verification, ACM Trans. Program. Lang. Syst. 16 (3) (1994) 843–871.

[43]

D. Harel, J. Tiuryn, D. Kozen, Dynamic Logic, MIT Press, 2000.

Digital Library

[44]

T. Henzinger, S. Qadeer, S. Rajamani, You assume, we guarantee: methodology and case studies, in: CAV'98, in: LNCS, vol. 1427, Springer-Verlag, 1998.

[45]

T.T. Hildebrandt, P. Panangaden, G. Winskel, A relational model of non-deterministic dataflow, Math. Struct. Comput. Sci. 14 (5) (2004) 613–649.

[46]

T.S. Hoang, J.-R. Abrial, Reasoning about liveness properties in event-B, in: Proceedings of the 13th International Conference on Formal Methods and Software Engineering, ICFEM'11, Springer-Verlag, Berlin, Heidelberg, 2011, pp. 456–471.

[47]

C.A.R. Hoare, An axiomatic basis for computer programming, Commun. ACM 12 (10) (1969) 576–580.

Digital Library

[48]

C.A.R. Hoare, Proof of correctness of data representations, Acta Inform. 1 (4) (Dec. 1972).

[49]

X. Jin, J. Deshmukh, J. Kapinski, K. Ueda, K. Butts, Benchmarks for model transformations and conformance checking, in: 1st Intl. Workshop on Applied Verification for Continuous and Hybrid Systems, ARCH, 2014.

[50]

X. Jin, J.V. Deshmukh, J. Kapinski, K. Ueda, K. Butts, Powertrain control verification benchmark, in: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC'14, ACM, 2014, pp. 253–262.

[51]

Y. Kesten, Z. Manna, A. Pnueli, Temporal verification of simulation and refinement, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (Eds.), A Decade of Concurrency Reflections and Perspectives: REX School/Symposium, Springer, 1994, pp. 273–346.

[52]

Y. Kesten, A. Pnueli, Complete proof system for QPTL, J. Log. Comput. 12 (5) (2002) 701.

[53]

L. Lamport, The temporal logic of actions, ACM Trans. Program. Lang. Syst. 16 (3) (May 1994) 872–923.

Digital Library

[54]

E. Lee, Y. Xiong, System-level types for component-based design, in: EMSOFT'01: 1st Intl. Workshop on Embedded Software, Springer, 2001, pp. 237–253.

[55]

B. Liskov, J. Wing, A behavioral notion of subtyping, ACM Trans. Program. Lang. Syst. 16 (6) (1994) 1811–1841.

Digital Library

[56]

R. Lublinerman, C. Szegedy, S. Tripakis, Modular code generation from synchronous block diagrams – modularity vs. code size, in: 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'09, ACM, Jan. 2009, pp. 78–89.

[57]

R. Lublinerman, S. Tripakis, Modularity vs. reusability: code generation from synchronous block diagrams, in: Design, Automation, and Test in Europe, DATE'08, ACM, Mar. 2008, pp. 1504–1509.

[58]

N. Lynch, M. Tuttle, An introduction to input/output automata, Quart. - Cent. Wiskd. Inform. 2 (1989) 219–246.

[59]

K. McMillan, A compositional rule for hardware design refinement, in: Computer Aided Verification, in: LNCS, vol. 1254, CAV'97, Springer-Verlag, 1997.

[60]

B. Meenakshi, A. Bhatnagar, S. Roy, Tool for translating Simulink models into input language of a model checker, in: Formal Methods and Software Engineering, in: LNCS, vol. 4260, Springer, 2006, pp. 606–620.

[61]

B. Meyer, Applying “Design by contract”, Computer 25 (10) (1992) 40–51.

[62]

S. Minopoli, G. Frehse, SL2SX translator: from Simulink to SpaceEx verification tool, in: 19th ACM International Conference on Hybrid Systems: Computation and Control, HSCC, 2016.

[63]

K.S. Namjoshi, R.J. Trefler, On the completeness of compositional reasoning methods, ACM Trans. Comput. Log. 11 (3) (2010).

[64]

O. Nierstrasz, Regular types for active objects, SIGPLAN Not. 28 (10) (1993) 1–15.

[65]

T. Nipkow, L.C. Paulson, M. Wenzel, Isabelle/HOL — a Proof Assistant for Higher-Order Logic, LNCS, vol. 2283, Springer, 2002.

[66]

P. Nuzzo, A. Iannopollo, S. Tripakis, A.L. Sangiovanni-Vincentelli, Are interface theories equivalent to contract theories?, in: 12th ACM-IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE, 2014.

[67]

A. Platzer, Differential dynamic logic for hybrid systems, J. Autom. Reason. 41 (2) (2008) 143–189.

[68]

A. Pnueli, The temporal logic of programs, in: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, IEEE Computer Society, 1977, pp. 46–57.

[69]

V. Preoteasa, I. Dragomir, S. Tripakis, Type inference of Simulink hierarchical block diagrams in Isabelle, in: 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE, 2017.

[70]

V. Preoteasa, I. Dragomir, S. Tripakis, Mechanically proving determinacy of hierarchical block diagram translations, in: VMCAI 2019 - 20th International Conference on Verification, Model Checking, and Abstract Interpretation, 2019.

[71]

V. Preoteasa, T. Latvala, K. Varpaaniemi, Modelling programmable logic controllers in refinement calculus of reactive systems, in: K. Ropiak, L. Polkowski, P. Artiemjew (Eds.), Proceedings of the 28th International Workshop on Concurrency, Specification and Programming, in: CEUR Workshop Proceedings, vol. 2571, Olsztyn, Poland, September 24-26th, 2019, 2019, CEUR-WS.org.

[72]

V. Preoteasa, S. Tripakis, Refinement calculus of reactive systems, in: 2014 International Conference on Embedded Software, EMSOFT, Oct 2014, pp. 1–10.

[73]

V. Preoteasa, S. Tripakis, Towards compositional feedback in non-deterministic and non-input-receptive systems, in: 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, 2016.

[74]

G. Reissig, A. Weber, M. Rungger, Feedback refinement relations for the synthesis of symbolic controllers, IEEE Trans. Autom. Control 62 (4) (2017) 1781–1796.

[75]

P.M. Rondon, M. Kawaguci, R. Jhala, Liquid types, in: 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '08, ACM, New York, NY, USA, 2008, pp. 159–169.

[76]

P. Roy, N. Shankar, SimCheck: an expressive type system for Simulink, in: C. Muñoz (Ed.), 2nd NASA Formal Methods Symposium, NFM 2010, NASA/CP-2010-216215, Langley Research Center, Hampton, VA 23681-2199, USA, Apr. 2010, pp. 149–160.

[77]

S. Sankaranarayanan, A. Tiwari, Relational abstractions for continuous and hybrid systems, in: Computer Aided Verification: 23rd International Conference, CAV 2011, Springer, 2011, pp. 686–702.

[78]

H. Schmeck, Algebraic characterization of reducible flowcharts, J. Comput. Syst. Sci. 27 (2) (1983) 165–199.

[79]

V. Sfyrla, G. Tsiligiannis, I. Safaka, M. Bozga, J. Sifakis, Compositional translation of Simulink models into synchronous BIP, in: 2010 International Symposium on Industrial Embedded Systems, SIES, July 2010, pp. 217–220.

[80]

N. Shankar, Lazy compositional verification, in: COMPOS'97: Revised Lectures from the International Symposium on Compositionality: the Significant Difference, Springer-Verlag, London, UK, 1998, pp. 541–564.

[81]

A. Siirtola, S. Tripakis, K. Heljanko, When do we not need complex assume-guarantee rules?, ACM Trans. Embed. Comput. Syst. 16 (2) (Jan. 2017) 48:1–48:25.

[82]

A.P. Sistla, M.Y. Vardi, P. Wolper, The complementation problem for Büchi automata with applications to temporal logic, Theor. Comput. Sci. 49 (1987) 217–237.

[83]

G. Stefănescu, Network Algebra, Springer-Verlag, New York, Inc., Secaucus, NJ, USA, 2000.

[84]

S. Tripakis, Compositionality in the science of system design, Proc. IEEE 104 (5) (May 2016) 960–972.

[85]

S. Tripakis, B. Lickly, T. Henzinger, E. Lee, On relational interfaces, in: Proceedings of the 9th ACM & IEEE International Conference on Embedded Software, EMSOFT'09, ACM, 2009, pp. 67–76.

[86]

S. Tripakis, B. Lickly, T.A. Henzinger, E.A. Lee, A theory of synchronous relational interfaces, ACM Trans. Program. Lang. Syst. 33 (4) (July 2011) 14:1–14:41.

Digital Library

[87]

S. Tripakis, C. Sofronis, P. Caspi, A. Curic, Translating discrete-time Simulink to lustre, ACM Trans. Embed. Comput. Syst. 4 (4) (Nov. 2005) 779–818.

Digital Library

[88]

S. Tripakis, C. Stergiou, M. Broy, E.A. Lee, Error-completion in interface theories, in: International SPIN Symposium on Model Checking of Software, in: LNCS, vol. 7976, SPIN 2013, Springer, 2013, pp. 358–375.

[89]

N. Wirth, Program development by stepwise refinement, Commun. ACM 14 (4) (1971) 221–227.

[90]

J. Woodcock, A. Cavalcanti, A tutorial introduction to designs in unifying theories of programming, in: E.A. Boiten, J. Derrick, G. Smith (Eds.), Integrated Formal Methods, Springer, 2004, pp. 40–66.

[91]

D. Yadav, M. Butler, Verification of liveness properties in distributed systems, in: Contemporary Computing, in: Communications in Computer and Information Science, vol. 40, Springer, Berlin, Heidelberg, 2009, pp. 625–636.

[92]

C. Yang, V. Vyatkin, Transformation of Simulink models to IEC 61499 Function Blocks for verification of distributed control systems, Control Eng. Pract. 20 (12) (2012) 1259–1269.

[93]

C. Zhou, R. Kumar, Semantic translation of Simulink diagrams to input/output extended finite automata, Discrete Event Dyn. Syst. 22 (2) (2012) 223–247.

[94]

L. Zou, N. Zhany, S. Wang, M. Franzle, S. Qin, Verifying Simulink diagrams via a hybrid Hoare logic prover, in: Embedded Software, EMSOFT, Sept 2013.

Cited By

Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103113
Bresolin DCollins PGeretti LSegala RVilla TŽivanović Gonzalez S(2024)A computable and compositional semantics for hybrid systemsInformation and Computation10.1016/j.ic.2024.105189300:COnline publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105189
Ishii D(2024)A Hypergraph-Based Formalization of Hierarchical Reactive Modules and a Compositional Verification MethodModel Checking Software10.1007/978-3-031-66149-5_4(67-84)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_4

Index Terms

The refinement calculus of reactive systems

Index terms have been assigned to the content through auto-classification.

Recommendations

A formal approach for the development of reactive systems

Context: This paper deals with the development and verification of liveness properties on reactive systems using the Event-B method. By considering the limitation of the Event-B method to invariance properties, we propose to apply the language TLA^+ to ...
The Refinement Calculus of Reactive Systems Toolset
Abstract
We present the Refinement Calculus of Reactive Systems Toolset, an environment for compositional formal modeling and reasoning about reactive systems, built around Isabelle, Simulink, and Python. The toolset implements the Refinement Calculus of ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Information and Computation

Information and Computation Volume 285, Issue PB

May 2022

998 pages

ISSN:0890-5401

Issue’s Table of Contents

Elsevier Inc.

Publisher

Academic Press, Inc.

United States

Publication History

Published: 01 May 2022

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 18 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Jesus JSampaio A(2024)Local deadlock analysis of Simulink models based on timed behavioural patterns and theorem provingScience of Computer Programming10.1016/j.scico.2024.103113236:COnline publication date: 1-Sep-2024
https://dl.acm.org/doi/10.1016/j.scico.2024.103113
Bresolin DCollins PGeretti LSegala RVilla TŽivanović Gonzalez S(2024)A computable and compositional semantics for hybrid systemsInformation and Computation10.1016/j.ic.2024.105189300:COnline publication date: 1-Oct-2024
https://dl.acm.org/doi/10.1016/j.ic.2024.105189
Ishii D(2024)A Hypergraph-Based Formalization of Hierarchical Reactive Modules and a Compositional Verification MethodModel Checking Software10.1007/978-3-031-66149-5_4(67-84)Online publication date: 10-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-66149-5_4

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents