zbMATH — the first resource for mathematics

SMT-based generation of symbolic automata. (English) Zbl 1443.68114
Summary: 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.
Reviewer: Reviewer (Berlin)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q55 Semantics in the theory of computing
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
CVC4; Kind 2; nuXmv; SMT-LIB; z3
Full Text: DOI
[1] Alberti, F.; Ghilardi, S.; Pagani, E.; Ranise, S.; Rossi, GP, Universal guards, relativization of quantifiers, and failure models in model checking modulo theories, JSAT, 8, 1-2, 29-61 (2012) · Zbl 1331.68141
[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) · Zbl 1350.68223
[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) · Zbl 1342.68029
[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) · Zbl 1275.68100
[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)
[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, TH; Sifakis, J., Rigorous component-based system design using the BIP framework, IEEE Softw., 28, 3, 41-48 (2011)
[9] Bliudze, S.; Henrio, L.; Madelaine, E.; Riis Nielson, H.; Tuosto, E., Verification of concurrent design patterns with data, Coordination Models and Languages, 161-181 (2019), Cham: Springer, Cham
[10] Bliudze, S.; Sifakis, J., The algebra of connectors—structuring interaction in BIP, IEEE Trans. Comput., 57, 10, 1315-1330 (2008) · Zbl 1390.68031
[11] Bliudze, S.; Sifakis, J., Causal semantics for the algebra of connectors, Form. Methods Syst. Des., 36, 2, 167-194 (2010) · Zbl 1207.68203
[12] Bruni, R.; de Frutos-Escrig, D.; Martí-Oliet, N.; Montanari, U.; Palamidessi, C., Bisimilarity congruences for open terms and term graphs via tile logic, CONCUR 2000, 259-274 (2000), Berlin: Springer, Berlin · Zbl 0999.68142
[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.; Biere, A.; Bloem, R., The nuXmv symbolic model checker, CAV, 334-342 (2014), Cham: Springer, Cham
[15] Champion, A.; Mebsout, A.; Sticksel, C.; Tinelli, C.; Chaudhuri, S.; Farzan, A., The kind 2 model checker, Computer Aided Verification, 510-517 (2016), Cham: Springer, Cham
[16] Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. CoRR arXiv:1310.6847 (2013) · Zbl 1368.68245
[17] De Simone, R., Higher-level synchronising devices in MEIJE-SCCS, Theor. Comput. Sci., 37, 245-267 (1985) · Zbl 0598.68027
[18] Déharbe, D., Integration of SMT-solvers in b and event-b development environments, Sci. Comput. Program., 78, 3, 310-326 (2013) · Zbl 1264.68056
[19] Déharbe, D.; Fontaine, P.; Guyot, Y.; Voisin, L., Integrating smt solvers in rodin, Sci. Comput. Program., 94, 130-143 (2014)
[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) · Zbl 1007.68135
[21] Feng, Y.; Deng, Y.; Ying, M., Symbolic bisimulation for quantum processes, ACM Trans. Comput. Log., 15, 2, 1-32 (2014) · Zbl 1291.68237
[22] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 1, 63-92 (2001) · Zbl 0973.68170
[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). 10.1007/978-3-540-71070-7_6 · Zbl 1165.68406
[24] Hennessy, M.; Lin, H., Symbolic bisimulations, Theor. Comput. Sci., 138, 2, 353-389 (1995) · Zbl 0874.68187
[25] Hennessy, M.; Rathke, J., Bisimulations for a calculus of broadcasting systems, Theor. Comput. Sci., 200, 1-2, 225-260 (1998) · Zbl 0915.68065
[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 · Zbl 1347.68267
[29] Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes – extended version. Rapport de recherche RR-8898, INRIA (2016) · Zbl 1347.68267
[30] Hoare, CAR, Communicating Sequential Processes (1985), Upper Saddle River: Prentice-Hall, Upper Saddle River · Zbl 0637.68007
[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). 10.4230/LIPIcs.CONCUR.2016.30 · Zbl 1392.68254
[33] Larsen, KG, A context dependent equivalence between processes, Theor. Comput. Sci., 49, 184-215 (1987) · Zbl 0612.68027
[34] Larsen, KG; Liu, X., Compositionality through an operational semantics of contexts, J. Log. Comput., 1, 6, 761-795 (1991) · Zbl 0738.68056
[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) · Zbl 0999.68141
[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). 10.4204/EPTCS.223.6 · Zbl 1433.68100
[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) · Zbl 0512.68026
[42] Milner, R., Communication and Concurrency. International Series in Computer Science (1989), Englewood Cliffs: Prentice-Hall, Englewood Cliffs · Zbl 0683.68008
[43] Milner, R., Communicating and Mobile Systems—the Pi-Calculus (1999), Cambridge: Cambridge University Press, Cambridge · Zbl 0942.68002
[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) · Zbl 1046.68626
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.