Top

Published in:

2019 | OriginalPaper | Chapter

Verification of Concurrent Design Patterns with Data

Authors : Simon Bliudze, Ludovic Henrio, Eric Madelaine

Published in: Coordination Models and Languages

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

We provide a solution for the design of safe concurrent systems by compositional application of verified design patterns—called architectures—to a small set of functional components. To this end, we extend the theory of architectures developed previously for the BIP framework with the elements necessary for handling data: definition and operations on data domains, syntax and semantics of composition operators involving data transfer. We provide a set of conditions under which composition of architectures preserves their characteristic safety properties. To verify that individual architectures do enforce their associated properties, we provide an encoding into open pNets, an intermediate model that supports SMT-based verification. The approach is illustrated by a case study based on a previously developed BIP model of a nanosatellite on-board software.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter No More, No Less

next chapter Self-organising Coordination Regions: A Pattern for Edge Computing

Only exported variables, belonging to a \(\varepsilon _{}(p)\), appear in the component interface (see Definition 7). We omit here this separation between internal and exported variables.

Notice that this definition allows \((\emptyset , \mathtt {t\!t}, \emptyset )\) and \((\emptyset , \mathtt {f\!f}, \emptyset )\) to be included in \(\varGamma \).

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). https://satassociation.org/jsat/index.php/jsat/article/view/93MathSciNetMATH

Ameur-Boulifa, R., Henrio, L., Kulankhina, O., Madelaine, E., Savu, A.: Behavioural semantics for asynchronous components. J. Log. Algebr. Methods Program. 89, 1–40 (2017). https://doi.org/10.1016/j.jlamp.2017.02.003, http://www.sciencedirect.com/science/article/pii/S2352220817300287MathSciNetCrossRef

Arnold, A.: Synchronised behaviours of processes and rational relations. Acta Inform. 17, 21–29 (1982)MathSciNetCrossRef

Aştefănoaei, L., Ben Rayana, S., Bensalem, S., Bozga, M., Combaz, J.: Compositional verification of parameterised timed systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 66–81. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_6CrossRef

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

Baranov, E.: A semantic framework for architecture modelling. Ph.D. thesis, EPFL (2017)

Basu, A., et al.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011). https://doi.org/10.1109/MS.2011.27MathSciNetCrossRef

Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69061-0CrossRefMATH

Bensalem, S., Bozga, M., Nguyen, T.H., Sifakis, J.: D-finder: a tool for compositional deadlock detection and verification. In: CAV, pp. 614–619 (2009). https://doi.org/10.1007/978-3-642-02658-4_45CrossRef

10.

Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-Finder 2: towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 453–458. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_32CrossRef

11.

Bliudze, S., et al.: Formal verification of infinite-state BIP models. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 326–343. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24953-7_25CrossRef

12.

Bliudze, S., Henrio, L., Madelaine, E.: Verification of concurrent design patterns with data. Technical report, Inria (2019, to appear)

13.

Bliudze, S., Sifakis, J.: The algebra of connectors–structuring interaction in BIP. In: Proceedings of the 7th ACM & IEEE International Conference on Embedded Software, EMSOFT 2007, pp. 11–20. ACM SigBED, Salzburg, October 2007. https://doi.org/10.1145/1289927.1289935

14.

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.26MathSciNetCrossRefMATH

15.

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-zCrossRefMATH

16.

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. LNCS, vol. 1877, pp. 259–274. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44618-4_20CrossRef

17.

Buisson, J., Calvacante, E., Dagnat, F., Leroux, E., Martinez, S.: Coqcots & Pycots: non-stopping components for safe dynamic reconfiguration. In: CBSE 2014: proceedings of the 17th International ACM SIGSOFT Symposium on Component-Based Software Engineering, Lille, France, p. 1, June 2014. https://hal.archives-ouvertes.fr/hal-00984365, https://doi.org/10.1145/2602458.2602459

18.

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

19.

Cansado, A., Madelaine, E.: Specification and verification for grid component-based applications: from models to tools. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 180–203. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04167-9_10CrossRef

20.

Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334–342. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_22CrossRef

21.

Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510–517. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_29CrossRef

22.

Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: IC3 modulo theories via implicit predicate abstraction. CoRR abs/1310.6847 (2013). http://arxiv.org/abs/1310.6847

23.

Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Log. Algebr. Program. 81(3), 227–256 (2012). https://doi.org/10.1016/j.jlap.2012.01.003. The 22nd Nordic Workshop on Programming Theory (NWPT 2010)MathSciNetCrossRef

24.

Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley Professional, Boston (1994)MATH

25.

Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Towards SMT model checking of array-based systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 67–82. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-71070-7_6CrossRef

26.

Hennessy, M., Lin, H.: Symbolic bisimulations. Theor. Comput. Sci. 138(2), 353–389 (1995)MathSciNetCrossRef

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 2015). IEEE (2015)

28.

Henrio, L., Kulankhina, O., Li, S., Madelaine, E.: Integrated environment for verifying and running distributed components. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 66–83. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_5CrossRef

29.

Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 175–194. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-39570-8_12CrossRefMATH

30.

Lin, H.: Symbolic transition graph with assignment. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 50–65. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61604-7_47CrossRef

31.

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

32.

Marmsoler, D.: Towards a theory of architectural styles. In: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pp. 823–825. ACM, New York (2014). https://doi.org/10.1145/2635868.2661683

33.

Marmsoler, D.: Hierarchical specification and verification of architectural design patterns. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 149–168. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89363-1_9CrossRef

34.

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)

35.

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

36.

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)

37.

Qiang, W., Bliudze, S.: Verification of component-based systems via predicate abstraction and simultaneous set reduction. In: Ganty, P., Loreti, M. (eds.) TGC 2015. LNCS, vol. 9533, pp. 147–162. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28766-9_10CrossRef

Title: Verification of Concurrent Design Patterns with Data
Authors: Simon Bliudze
Ludovic Henrio
Eric Madelaine
Publisher: Springer International Publishing
Book: Coordination Models and Languages
Print ISBN: 978-3-030-22396-0

Electronic ISBN: 978-3-030-22397-7

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-22397-7_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner