nach oben

Software and Systems Modeling

Erschienen in:

24.04.2014 | Regular Paper

Component-based verification using incremental design and invariants

verfasst von: Saddek Bensalem, Marius Bozga, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan

Erschienen in: Software and Systems Modeling | Ausgabe 2/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are obtained by combining local invariants of their constituent components with interaction invariants that take interactions into account. We study new techniques for computing interaction invariants. Some of these techniques are incremental, i.e., interaction invariants of a composite hierarchically structured component are computed by reusing invariants of its constituents. We formalize incremental construction of components in the BIP language as the process of building progressively complex components by adding interactions (synchronization constraints) to atomic components. We provide sufficient conditions ensuring preservation of invariants when new interactions are added. When these conditions are not satisfied, we propose methods for generating new invariants in an incremental manner by reusing existing invariants from the constituents in the incremental construction. The reuse of existing invariants reduces considerably the overall verification effort. The techniques have been implemented in the D-Finder toolset. Among the experiments conducted, we have been capable of verifying safety properties and deadlock-freedom of sub-systems of the functional level of the DALA autonomous robot. This work goes far beyond the capacity of existing monolithic verification tools.

Vorheriger Artikel A situational method for semi-automated Enterprise Architecture Documentation

Nächster Artikel Formalizing and verifying stochastic system architectures using Monterey Phoenix

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

See Sect. 6 for detailed explanation.

See http://www.bip-components.com for the complete list.

http://www-verimag.imag.fr/ASCENS.html.

http://www-verimag.imag.fr/PRO3D.html.

http://www-verimag.imag.fr/ACROSS.html.

If an interaction only allows two ports, the composite component returns to the traditional transition system with pair-wise synchronization

As increments are sets of interactions, we use \(\oplus \) for the union between two increments.

We admit that the comparison is unfair for NuSMV. The reason being that D-Finder does not explore the reachable state space.

A succinct description of the Utopar case study can be found at http://www.combest.eu/home/?link=Application2.

The latter can be seen as an abstraction of the component in where some services have been removed.

Abdellatif, T., Combaz, J., Sifakis J.: Model-based implementation of real-time applications. In: EMSOFT, pp. 229–238, Scottsdale, AZ, USA (2010)

Alfaro, L.D., Henzinger, T.A.: Interface theories for component-based design. In: EMSOFT, pp. 148–165. Springer (2001)

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

Balarin, F., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A., Sgroi, M., Watanabe Y.: Modeling and designing heterogeneous systems. In: Concurrency and Hardware Design, pp. 228–273 (2002)

Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft. In: IFM, pp. 1–20. Springer (2004)

Ball, T., Rajamani, S.K.: The SLAM toolkit. In: CAV, pp. 260–264 (2001)

Ball, T., Rajamani S.K.: The SLAM project: debugging system software via static analysis. In: POPL, pp. 1–3 (2002)

Basu, A., Bensalem, S., Bozga, M., Bourgos, P., Maheshwari, M., Sifakis, J.: Component assemblies in the context of manycore. In: FMCO, pp. 314–333 (2011)

Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: FMOODS/FORTE, vol. 6117, LNCS, pp. 32–46. Springer (2010)

10.

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)CrossRef

11.

Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: RV, pp. 330–344. Springer (2010)

12.

Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in BIP. In: SEFM, pp. 3–12. IEEE Computer Society (2006)

13.

Basu, A., Mounier, L., Poulhis, M., Pulou, J., Sifakis, J.: Using BIP for modeling and verification of networked systems—a case study on tinyos-based networks. In: NCA, pp. 257–260 (2007)

14.

Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A., Nouri, A.: Statistical model checking qos properties of systems with SBIP. In: ISOLA, pp. 327–341 (2012)

15.

Bensalem, S., Bozga, M., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Incremental component-based construction and verification using invariants. In: FMCAD, pp. 257–265 (2010)

16.

Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: Compositional verification for component-based systems and application. In: ATVA, pp. 64–79. Springer (2008)

17.

Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis J.: D-Finder: A tool for compositional deadlock detection and verification. In: CAV, pp. 614–619. Springer (2009)

18.

Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: Compositional verification for component-based systems and application. IET Softw. 4, 179–235 (2010)CrossRefMATH

19.

Bensalem, S., de Silva, L., Gallien, M., Ingrand, F., Yan, R.: “Rock solid” software: a verifiable and correct by construction controller for rover and spacecraft functional layers. In: ISAIRAS, pp. 859–866 (2010)

20.

Bensalem, S., de Silva, L., Griesmayer, A., Ingrand, F., Legay, A., Yan, R.: A formal approach for incremental construction with an application to autonomous robotic systems. In: SC, vol. 6708, pp. 116–132. Springer (2011)

21.

Bensalem, S., Gallien, M., Ingrand, F., Kahloul, I., Nguyen, T.-H.: Toward a more dependable software architecture for autonomous robots. IEEE Robot. Autom. Mag. 16(1), 1–11 (2009)CrossRef

22.

Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Peled, D.: Efficient deadlock detection for concurrent systems. In: MEMOCODE, pp. 119–129 (2011)

23.

Bensalem, S., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Incremental invariant generation for compositional design. In: TASE, pp. 157–167 (2010)

24.

Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST: applications to software engineering. STTT 9(5–6), 505–525 (2007)CrossRef

25.

BIP. http://www-verimag.imag.fr/BIP,196.html?

26.

Bliudze, S., Sifakis, J.: The algeba of connectors—structuring interaction in BIP. IEEE Trans. Comput. 57, 1315–1330 (October 2008)

27.

Bluespec. http://www.bluespec.com/

28.

Bozga, M., Jaber, M., Maris, N., Sifakis, J.: Modeling dynamic architectures using Dy-BIP. In: SC, pp. 1–16. Springer, Berlin (2012)

29.

Bozga, M., Sfyrla, V., Sifakis, J.: Modeling synchronous Systems in BIP. In: EMSOFT, pp. 77–86. ACM, October (2009)

30.

Chandy, K.M.: Parallel Program Design: A Foundation. Addison-Wesley Longman, Boston (1988)MATH

31.

Chaudron, M.R.V., Eskenazi, E.M., Fioukov, A.V., Hammer D.K.: A framework for formal component-based software architecting. In: SAVCBS, pp. 73–80 (2001)

32.

Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. In: FSTTCS, pp. 326–337. Springer, London, UK (1993)

33.

Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2, 410–425 (2000)CrossRefMATH

34.

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)

35.

Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning. ACM Trans. Softw. Eng. Methodol. 17(2), 1–52 (2008)CrossRef

36.

Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: TACAS, pp. 331–346 (2003)

37.

Combest. http://www.combest.eu/home/

38.

Conway, C.L., Namjoshi, K.S., Dams, D., Edwards, S.A.: Incremental algorithms for inter-procedural analysis of safety properties. In: CAV, pp. 449–461. Springer (2005)

39.

Cook, B., Podelski, A., Rybalchenko, A.: Terminator: beyond safety. In: CAV, pp. 415–418 (2006)

40.

David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed i/o automata: A complete specification theory for real-time systems. In: HSCC, pp. 91–100. ACM, New York, NY, USA (2010)

41.

David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: HSCC, pp. 91–100 (2010)

42.

de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: FroCos, pp. 81–105 (2005)

43.

de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press, Cambridge (2000)MATH

44.

Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: CAV, pp. 81–94. Springer (2006)

45.

Farzan, A., Chen, Y.-F., Clarke, E. M., Tsay, Y.-K. , Wang, B.-Y.: Extending automated compositional verification to the full class of omega-regular languages. In: TACAS, pp. 2–17. Springer (2008)

46.

Flanagan, C., Qadeer, S.: Thread-modular model checking. In: SPIN, pp. 213–224. Springer (2003)

47.

Fleury, S., Herrb, M., Chatila, R.: GenoM: a tool for the specification and the implementation of operating modules in a distributed robot architecture. In: IROS, pp. 842–848 (1997)

48.

Fritzson, P., Engelson, V.: Modelica a unified object-oriented language for system modeling and simulation. In: ECOOP, pp. 67–90 (1998)

49.

Giannakopoulou, D., Păsăreanu, C. S., Barringer, H.: Assumption generation for software component verification. In: ASE, pp. 3–12. IEEE Computer Society (2002)

50.

Gößler, G., Sifakis,. J.: Priority systems. In: FMCO, pp. 314–329 (2003)

51.

Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, pages 331–344. ACM, 2011

52.

Heimbold, D., Luckham, D.: Debugging Ada tasking programs. IEEE Softw. 2(2), 47–57 (1985)CrossRef

53.

Henzinger, T.A., Hottelier, T., Kovács, L., Rybalchenko, A.: Aligators for arrays. In: LPAR, TACAS, pp. 348–356 (2010)

54.

Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70. ACM (2002)

55.

Henzinger, T.A., Qadeer, S., Rajamani, S. K.: You assume, we guarantee: methodology and case studies. In: CAV, pp. 440–451. Springer (1998)

56.

Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.J.: Incremental analysis of constraint logic programs. ACM Trans. Program. Lang. Syst. 22(2), 187–223 (Mar. 2000)

57.

Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

58.

Khendek, F., Bochmann, G.V.: Incremental construction approach for distributed system specifications. In: Proceedings of the International Symposium on Formal Description, Techniques, pp. 26–29 (1993)

59.

Larsen, K.G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems, pp. 232–246 (1989)

60.

Lau, K.-K., Ng, K.-Y., Rana,T., Tran, C.M.: Incremental construction of component-based systems. In: CBSE, pp. 41–50. ACM, New York, NY, USA (2012)

61.

Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Q. 2, 219–246 (1989)MathSciNetMATH

62.

Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)CrossRefMATH

63.

Moura, L.D., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS, pp. 337–340. Springer (2008)

64.

Nguyen, T.-H.: Constructive Verification of Component-Based Systems. PhD Thesis, Institut National Polytechnique de Grenoble (2010)

65.

Patil, S.S.: Limitations and Capabilities of Dijkstra’s Semaphore Primitives for Coordination among Processes. Cambridge, MA: MIT, Project MAC, Computation Structures Group Memo 57, Feb (1971)

66.

Pnueli, A.: In transition from global to modular temporal reasoning about programs. Log. Models Concurr. Syst. F13, 123–144 (1985)MathSciNetCrossRefMATH

67.

Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: TACAS, pp. 237–251 (2012)

68.

Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: ICALP, pp. 337–351. Springer (1982)

69.

Somenzi, F.: CUDD: CU decision diagram package

70.

Team, O.: The Omega, library (1996)

71.

Thiele, L., Bacivarov, I., Haid, W., Huang, K.: Mapping Applications to Tiled Multiprocessor Embedded Systems. In: ACSD, pp. 29–40. IEEE Computer Society (2007)

72.

Tripakis, S., Stergiou, C., Shaver, C., Lee, E.A.: A modular formal semantics for ptolemy. Math. Struct. Comput. Sci. 23, 834–881 (2013)

Titel: Component-based verification using incremental design and invariants
verfasst von: Saddek Bensalem
Marius Bozga
Axel Legay
Thanh-Hung Nguyen
Joseph Sifakis
Rongjie Yan
Publikationsdatum: 24.04.2014
Verlag: Springer Berlin Heidelberg
Erschienen in: Software and Systems Modeling / Ausgabe 2/2016
Print ISSN: 1619-1366
Elektronische ISSN: 1619-1374
DOI: https://doi.org/10.1007/s10270-014-0410-8

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2016

Effective application of process improvement patterns to business processes

A situational method for semi-automated Enterprise Architecture Documentation

Service feature modeling: modeling and participatory ranking of service design alternatives

A framework for the operationalization of monitoring in business intelligence requirements engineering

Heuristic search for equivalence checking

View-based model-driven software development with ModelJoin