[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

SMT-based generation of symbolic automata

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

Abstract

Open pNets are formal models that can express the behaviour of open systems, either synchronous, asynchronous, or heterogeneous. They are endowed with a symbolic operational semantics in terms of open automata, which allows us to check properties of such systems in a compositional manner. We present an algorithm computing these semantics, building predicates expressing the synchronisation conditions between the events of pNet sub-systems. Checking such predicates requires symbolic reasoning about first order logics and application-specific data. We use the Z3 SMT engine to check satisfiability of the predicates. We also propose and implement an optimised algorithm that performs part of the pruning on the fly, and show its correctness with respect to the original one. We illustrate the approach using two use-cases: the first one is a classical process-algebra operator for which we provide several encodings, and prove some basic properties. The second one is industry-oriented and based on the so-called “BIP architectures”, which have been used to specify the control software of a nanosatellite at the EPFL Space Engineering Center. We use pNets to encode a BIP architecture extended with explicit data, compute its semantics and discuss its properties, and then show how our algorithms scale up, using a composition of two such architectures.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10

Similar content being viewed by others

Notes

  1. For convenience, we provide these rules and the proof of the finiteness theorem in “Appendix 1”.

  2. The original CubETH case study [40] focused on the possibility of assembling a model of a complex software system in a systematic way by applying architectures to discharge individual system requirements. Here, we are more interested in the properties of the Failure Monitor architecture by itself. For that reason, we provide a modified version, in particular decomposing the coordinator into a Controller and a Timer, altering them to allow more flexibility in the acceptable behaviours. In other words, this modification enforces similar properties, while discarding less acceptable behaviours.

  3. One of the main results of [3] states that in a system obtained by an application of several architectures, liveness properties are preserved if these architectures are pair-wise non-interfering. However, no results were provided to check whether two architectures are interfering or not.

  4. Available at https://team.inria.fr/scale/software/vercors/.

References

  1. Alberti, F., Ghilardi, S., Pagani, E., Ranise, S., Rossi, G.P.: Universal guards, relativization of quantifiers, and failure models in model checking modulo theories. JSAT 8(1/2), 29–61 (2012)

    MathSciNet  MATH  Google Scholar 

  2. Armand, M., Faure, G., Grégoire, B., Keller, C., Théry, L., Werner, B.: A modular integration of sat/smt solvers to coq through proof witnesses. In: International Conference on Certified Programs and Proofs, pp. 135–150. Springer, Berlin (2011)

  3. Attie, P., Baranov, E., Bliudze, S., Jaber, M., Sifakis, J.: A general framework for architecture composability. Form. Asp. Comput. 18(2), 207–231 (2016)

    Article  MathSciNet  Google Scholar 

  4. Baldan, P., Bracciali, A., Bruni, R.: Bisimulation by unification. In: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science, vol. 2422, pp. 254–270. Springer (2002)

  5. Baranov, E., Bliudze, S.: Offer semantics: achieving compositionality, flattening and full expressiveness for the glue operators in BIP. Sci. Comput. Program. 109, 2–35 (2015). https://doi.org/10.1016/j.scico.2015.05.011

    Article  Google Scholar 

  6. Barrett, C., Conway, C., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: Cvc4. In: Computer Aided Verification, Springer (2011)

  7. Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org

  8. Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011). https://doi.org/10.1109/MS.2011.27

    Article  Google Scholar 

  9. Bliudze, S., Henrio, L., Madelaine, E.: Verification of concurrent design patterns with data. In: Riis Nielson, H., Tuosto, E. (eds.) Coordination Models and Languages, pp. 161–181. Springer, Cham (2019)

    Chapter  Google Scholar 

  10. Bliudze, S., Sifakis, J.: The algebra of connectors—structuring interaction in BIP. IEEE Trans. Comput. 57(10), 1315–1330 (2008). https://doi.org/10.1109/TC.2008.26

    Article  MathSciNet  MATH  Google Scholar 

  11. Bliudze, S., Sifakis, J.: Causal semantics for the algebra of connectors. Form. Methods Syst. Des. 36(2), 167–194 (2010). https://doi.org/10.1007/s10703-010-0091-z

    Article  MATH  Google Scholar 

  12. Bruni, R., de Frutos-Escrig, D., Martí-Oliet, N., Montanari, U.: Bisimilarity congruences for open terms and term graphs via tile logic. In: Palamidessi, C. (ed.) CONCUR 2000, pp. 259–274. Springer, Berlin (2000)

    Chapter  Google Scholar 

  13. Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Verification of data-aware processes via array-based systems (extended version). CoRR arXiv:1806.11459 (2018)

  14. Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV, pp. 334–342. Springer, Cham (2014)

    Google Scholar 

  15. Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification, pp. 510–517. Springer, Cham (2016)

    Chapter  Google Scholar 

  16. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. CoRR arXiv:1310.6847 (2013)

  17. De Simone, R.: Higher-level synchronising devices in MEIJE-SCCS. Theor. Comput. Sci. 37, 245–267 (1985)

    Article  MathSciNet  Google Scholar 

  18. Déharbe, D.: Integration of SMT-solvers in b and event-b development environments. Sci. Comput. Program. 78(3), 310–326 (2013)

    Article  Google Scholar 

  19. Déharbe, D., Fontaine, P., Guyot, Y., Voisin, L.: Integrating smt solvers in rodin. Sci. Comput. Program. 94, 130–143 (2014)

    Article  Google Scholar 

  20. Deng, Y., Fu, Y.: Algorithm for verifying strong open bisimulation in full \(\pi \) calculus. J. Shanghai Jiaotong Univ. E–5(2), 147–152 (2001)

    MATH  Google Scholar 

  21. Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. ACM Trans. Comput. Log. 15(2), 1–32 (2014)

    Article  MathSciNet  Google Scholar 

  22. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1), 63–92 (2001). https://doi.org/10.1016/S0304-3975(00)00102-X

    Article  MathSciNet  MATH  Google Scholar 

  23. Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, 2008, pp. 67–82 (2008). https://doi.org/10.1007/978-3-540-71070-7_6

  24. Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353–389 (1995). https://doi.org/10.1016/0304-3975(94)00172-F

    Article  MathSciNet  MATH  Google Scholar 

  25. Hennessy, M., Rathke, J.: Bisimulations for a calculus of broadcasting systems. Theor. Comput. Sci. 200(1–2), 225–260 (1998). https://doi.org/10.1016/S0304-3975(97)00261-2

    Article  MathSciNet  MATH  Google Scholar 

  26. Henrio, L., Kulankhina, O., Liu, D., Madelaine, E.: Verifying the correct composition of distributed components: Formalisation and Tool. In: FOCLASA, no. 175 in EPTCS. Rome (2014). https://hal.inria.fr/hal-01055370

  27. Henrio, L., Madelaine, E., Zhang, M.: pNets: an expressive model for parameterised networks of processes. In: 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP’15). IEEE (2015)

  28. Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Formal Techniques for Distributed Objects, Components, and Systems (FORTE), vol. LNCS-9688. Heraklion, Greece (2016). https://hal.inria.fr/hal-01432917

  29. Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes – extended version. Rapport de recherche RR-8898, INRIA (2016)

  30. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  31. ISO: Information Processing Systems—Open Systems Interconnection—LOTOS—A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807, International Organisation for Standardization, Geneva, Switzerland (1989). citeseer.ist.psu.edu/338220.html

  32. Konnov, I.V., Kotek, T., Wang, Q., Veith, H., Bliudze, S., Sifakis, J.: Parameterized systems in BIP: design and model checking. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, LIPIcs, vol. 59, pp. 30:1–30:16 (2016). https://doi.org/10.4230/LIPIcs.CONCUR.2016.30

  33. Larsen, K.G.: A context dependent equivalence between processes. Theor. Comput. Sci. 49, 184–215 (1987)

    Article  Google Scholar 

  34. Larsen, K.G., Liu, X.: Compositionality through an operational semantics of contexts. J. Log. Comput. 1(6), 761–795 (1991)

    Article  MathSciNet  Google Scholar 

  35. Leifer, J.J., Milner, R.: Deriving bisimulation congruences for reactive systems. In: The 11th International Conference on Concurrency Theory, Lecture Notes in Computer Science, vol. 1877, pp. 243–258. Springer (2000)

  36. Li, Z.: Theories and algorithms for the verification of bisimulation equivalences in value-passing CCS and \(\pi \)-calculus. Ph.D. thesis, Changsha Institute of Technology (1999)

  37. Lin, H.: Symbolic transition graph with assignment. In: Montanari, U., Sassone, V. (eds.) Concur’96, LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996)

  38. Lin, H.: Model checking value-passing processes. In: 8th Asia-Pacific Software Engineering Conference (APSEC’2001). Macau (2001)

  39. Mavridou, A., Baranov, E., Bliudze, S., Sifakis, J.: Architecture diagrams: a graphical language for architecture style specification. In: Proceedings 9th Interaction and Concurrency Experience (ICE), EPTCS, vol. 223, pp. 83–97 (2016). https://doi.org/10.4204/EPTCS.223.6

  40. Mavridou, A., Stachtiari, E., Bliudze, S., Ivanov, A., Katsaros, P., Sifakis, J.: Architecture-based design: a satellite on-board software case study. In: 13th International Conference on Formal Aspects of Component Software (FACS 2016) (2016)

  41. Milner, R.: Calculi for synchrony and asynchrony. TCS 25(3), 267–310 (1983). https://doi.org/10.1016/0304-3975(83)90114-7

    Article  MathSciNet  MATH  Google Scholar 

  42. Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1989). SU Fisher Research 511/24

    Google Scholar 

  43. Milner, R.: Communicating and Mobile Systems—the Pi-Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  44. Qin, X., Bliudze, S., Madelaine, E., Zhang, M.: Using SMT engine to generate symbolic automata. In: 18th International Workshop on Automated Verification of Critical Systems (AVOCS 2018). Electronic Communications of the EASST (2018)

  45. Qin, X., Bliudze, S., Madelaine, E., Zhang, M.: Using SMT engine to generate Symbolic Automata—Extended version. Rapport de recherche RR-9177, INRIA (2018)

  46. Rensink, A.: Bisimilarity of open terms. Inf. Comput. 156(1–2), 345–385 (2000)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, MOE International Joint Lab of Trustworthy Software, International Research Center of Trustworthy Software, East China Normal University, Shanghai, and Peng Cheng Laboratory, Shenzhen, China

    Xudong Qin, Zechen Hou, Yuxin Deng & Min Zhang

  2. Inria Lille – Nord Europe, 40 Avenue Halley, 59650, Villeneuve d’Ascq, France

    Simon Bliudze

  3. Université Côte d’Azur, Inria, CNRS, I3S, 06902, Sophia Antipolis, France

    Eric Madelaine

Authors
  1. Xudong Qin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Bliudze
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eric Madelaine
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zechen Hou
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Yuxin Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Min Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yuxin Deng.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This work was partially supported by the National Natural Science Foundation of China (61672229, 61832015, 61672012), the Associated Team FM4CPS between INRIA and ECNU, and the Inria-CAS joint project Quasar.

Appendix A Semantic rules of pNets

Appendix A Semantic rules of pNets

To facilitate the understanding of the two algorithms, we briefly recall the semantic rules of pNets, more details can be found in [28].

We build the semantics of an open pNet as an open automaton where LTSs are the PLTSs at the pNet leaves, and the states of the automaton are structured. To build an open transition we first projects the global state into states of the leaves, then apply PLTS transitions on these states, and compose them with actions of holes using synchronisation vectors.

The semantics regularly instantiates fresh variables, and uses a clone operator that clones a term replacing each variable with a fresh one. The variables in each synchronisation vector are considered local: for a given pNet expression, we must have fresh local variables for each occurrence of a vector. Similarly, the state variables of each copy of a given PLTS in the system must be distinct, and those created for each application of Tr2 have to be fresh and all distinct.

The reader may notice that the structure of OTs produced by these rules is richer than the one from the definitions in Sect. 4, as they contain information about the leaves transitions in each OT. This is also the case in the implementation, and provides us with tracability and debugging features in the tool.

Definition 6

(Operational semantics of open pNets) The semantics of a pNet p is an open automaton \(A = \langle Leaves(p),J,\mathcal {S}, s_0, \mathcal {T}\rangle \) where:

  • J is the indices of the holes: \(Holes(p)= H_j^{j\in J}\).

  • \(\overline{\mathcal {S}} = States(p)\) and \(s_0 = InitState(p)\)

  • \(\mathcal {T}\) is the smallest set of open transitions satisfying the rules below:

The first rule (Tr1) for a PLTS p checks that the guard is verified and transforms assignments into post-conditions:

Tr1::

The second rule (Tr2) deals with pNet nodes: for each possible synchronisation vector applicable to the rule subject, the premisses include one open transition for each sub-pNet involved, one possible action for each hole involved, and the predicate relating these with the resulting action of the vector. A key to understand this rule is that the open transitions are expressed in terms of the leaves and holes of the pNet structure, i.e. a flatten view of the pNet. For example, in the rule, L is the index set of the leaves of the open pNet, \(L_k\) is the index set of the leaves of one subnet, thus all \(L_k\) are disjoint subsets of L.

Tr2::

In rule TR2, the generated predicate is composed of the conjunction of the predicates of the subnets’ OTs, with the additional part encoding the application of the chosen synchronisation vector. In [28] this last part is defined as:

$$\begin{aligned} {\textit{MkPred}}(SV_k, a_i^{i\in I}, b_j^{j\in J}, v)\Leftrightarrow SV_k={(a_i)}^{i\in I}, {(b_j)}^{j\in J}\rightarrow v \end{aligned}$$

Within Algorithm 1, these subsets have been computed by the Combining method and passed as arguments to the Matching method (cf. Sect. 4)

To have some practical interest, it is important to know when Algorithm 1 terminates. The following theorem shows that if an open pNet has finite synchronisation sets, finitely many leaves and holes, and each PLTS at its leaves has a finite number of states and (symbolic) transitions, then Algorithm 1 terminates and the operational semantics of the open pNet is a finite automaton.

Theorem 4

(Finiteness) [28] Let \(pnet=\langle \overline{{\textit{pNet}}},\overline{S}, {\textit{SV}}_k^{k\in K}\rangle \) be an open pNet with leaves \(l_i^{i\in I}\) and holes \(h_j^{j\in J}\), where the sets I and J are finite. Suppose the synchronisation vectors of all pNets included in pnet are finite, and \(l_i \) has a finite number of state variables for each \(i\in I\). Then the semantics of pnet is an open automaton with finitely many states and transitions.

Proof

The possible set of states of the open automaton is the cartesian product of the states of the pNet \(PLTS_i^{i\in I}\), which is finite by hypothesis. So the top-level residual loop of Algorithm 1 terminates provided each iteration terminates. The enumeration of open-transitions in line 5 of Algorithm 1 is bounded by the number of applications of rule Tr2 on the structure of the pNet tree. Since a finite number of synchronisation vectors are applied at each node, the number of global open transitions is finite. Similarily, if the number of transitions of each PLTS is finite, rule Tr1 is applied a finite number of times. Therefore, each internal loop of Algorithm 1 terminates, and we obtain finitely many deduction trees and open transitions. \(\square \)

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Qin, X., Bliudze, S., Madelaine, E. et al. SMT-based generation of symbolic automata. Acta Informatica 57, 627–656 (2020). https://doi.org/10.1007/s00236-020-00367-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-020-00367-6

Search

Navigation