zbMATH — the first resource for mathematics

A verification-driven framework for iterative design of controllers. (English) Zbl 1425.68262
Summary: Controllers often are large and complex reactive software systems and thus they typically cannot be developed as monolithic products. Instead, they are usually comprised of multiple components that interact to provide the desired functionality. Components themselves can be complex and in turn be decomposed into multiple sub-components. Designing such systems is complicated and must follow systematic approaches, based on recursive decomposition strategies that yield a modular structure. This paper proposes FIDDle – a comprehensive verification-driven framework which provides support for designers during development. FIDDle supports hierarchical decomposition of components into sub-components through formal specification in terms of pre- and post-conditions as well as independent development, reuse and verification of sub-components. The framework allows the development of an initial, partially specified design of the controller, in which certain components, yet to be defined, are precisely identified. These components can be associated with pre- and post-conditions, i.e., a contract, that can be distributed to third-party developers. The framework ensures that if the components are compliant with their contracts, they can be safely integrated into the initial partial design without additional rework. As a result, FIDDle supports an iterative design process and guarantees correctness of the system at any step of development. We evaluated the effectiveness of FIDDle in supporting an iterative and incremental development of components using the K9 Mars Rover example developed at NASA Ames. This can be considered as an initial, yet substantive, validation of the approach in a realistic setting. We also assessed the scalability of FIDDle by comparing its efficiency with the classical model checkers implemented within the LTSA toolset. Results show that FIDDle scales as well as classical model checking as the number of the states of the components under development and their environments grow.
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68N99 Theory of software
68Q45 Formal languages and automata
Full Text: DOI
[1] Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-oriented software product lines. Springer, Berlin (2016)
[2] Akesson K, Fabian M, Flordal H, Malik R (2006) Supremica—An integrated environment for verification, synthesis and simulation of discrete event systems. In: Proceedings of WODES’06. IEEE, pp 384-385
[3] Amalfitano D, Fasolino AR, Tramontana P (2008) Reverse engineering finite state machines from rich Internet applications. In: Proceedings of WCRE’08, pp 69-73
[4] Alur, R.; Henzinger, TA, No article title, Reactive modules. Formal Methods Softw Des, 15, 7-48 (1999)
[5] Alur R, Moarref S, Topcu U (2013) Counter-strategy guided refinement of GR(1) temporal logic specifications. In: Proceedings of FMCAD’13, IEEE, pp 26-33
[6] Alur R, Moarref S, Topcu U (2015) Pattern-based refinement of assume-guarantee specifications in reactive synthesis. In: Proceedings of TACAS’15. Springer, Berlin, pp 501-516 · Zbl 1420.68116
[7] Alur R, Moarref S, Topcu U (2016) Compositional synthesis of reactive controllers for multi-agent systems. In: Proceedings of CAV’16. Springer, Berlin, pp 251-269 · Zbl 1411.68156
[8] Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM SIGSOFT Softw Eng Notes 23(6), 175-188 (1998)
[9] Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans Program Lang Syst (TOPLAS) 23(3), 273-303 (2001)
[10] Bensalem S, Bozga M, Krichen M, Tripakis S (2004) Testing conformance of real-time applications by automatic generation of observer. In: Proceedings of RV’04. Electronic Notes in Theoretical Computer Science, pp 23-43
[11] Belguidoum, M., Dagnat, F.: Formalization of component substitutability. Electron Notes Theor Comput Sci 215, 75-92 (2008)
[12] Blom, S.; Darabi, S.; Huisman, M., Verification of loop parallelisations, 202-217 (2015), Berlin
[13] Bruns G, Godefroid P (1999) Model checking partial state spaces with 3-valued temporal logics. In: Proceedings of CAV’99, volume 1633 of LNCS, pp 274-287 · Zbl 1046.68583
[14] Bernasconi, A.; Menghi, C.; Spoletini, P.; Zuck, LD; Ghezzi, C., From model checking to a temporal proof for partial models, 54-69 (2017), Berlin · Zbl 1420.68118
[15] Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Softw Tools Technol Transf 17(6), 729-744 (2015)
[16] Büchi, JR, On a decision method in restricted second order arithmetic, 425-435 (1990), Berlin
[17] Ciolek D, Braberman VA, D’Ippolito N, Uchitel S (2016) Technical report: directed controller synthesis of discrete event systems. arXiv:1605.09772
[18] Chechik M, Brunet G, Fischbein D, Uchitel S (2006) Partial behavioural models for requirements and early design. In: Proceedings of Dagstuhl seminar MMOSS, p 6351
[19] Cimatti A, Clarke E, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A (2002) NuSMV 2: an opensource tool for symbolic model checking. In: Proceedings of CAV’02. Springer, Berlin, pp 359-364 · Zbl 1010.68766
[20] Chaki, S., Clarke, E.M., Sharygina, N., Sinha, N.: Verification of evolving software via component substitutability analysis. Formal Methods Softw Des 32(3), 235-266 (2008) · Zbl 1147.68047
[21] Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans Softw Eng Methodol (TOSEM) 12(4), 371-408 (2003) · Zbl 1109.68063
[22] Calvanese D, De Giacomo G, Vardi MY (2002) Reasoning about actions and planning in LTL action theories. In: Proceedings of KR’02, volume 2, pp 593-602
[23] Clarke, E.M.: Orna Grumberg, and Doron Peled. MIT Press, Cambridge, Model checking (1999)
[24] Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of TACAS’03. Springer, Berlin, pp 331-346 · Zbl 1031.68545
[25] Councill, W.T., Heineman, G.T.: Component-based software engineering: putting the pieces together, pp. 5-99. Addison Wesley, New York (2001)
[26] Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor Comput Sci 484, 1-15 (2013) · Zbl 1292.68107
[27] Li HC, Krishnamurthi S, Fisler K (2002) Interfaces for modular feature verification. In: Proceedings 17th IEEE international conference on automated software engineering, pp 195-204
[28] Cok, DR, OpenJML: JML for Java 7 by extending OpenJDK, 472-479 (2011), Berlin
[29] Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong and strong ycling Planning via symbolic model checking. Technical report, IRST (2015) · Zbl 1082.68800
[30] Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci Comput Programming 97, 333-348 (2015)
[31] Dwyer MB, Avrunin GS, Corbett JC (1998) Property Specification patterns for finite-state verification. In: Proceedings of FMSP’98. ACM, pp 7-15
[32] de Alfaro Luca, Henzinger Thomas A (2001) Interface automata. In Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on foundations of software engineering, ESEC/FSE-9. ACM, New York, pp 109-120
[33] D’Ippolito N, Braberman V, Piterman N, Uchitel S (2010) Synthesis of live behaviour models. In: Proceedings of SIGSOFT FSE’10. ACM, pp 77-86
[34] D’Ippolito N, Braberman V, Piterman N, Uchitel S (2011) Synthesis of live behaviour models for fallible domains. In: Proceedings of ICSE’11. IEEE, pp 211-220
[35] D’Ippolito N, Braberman V, Piterman N, Uchitel S (2013) Synthesising non-anomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22
[36] De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of IJCAI. ACM, pp 854-860
[37] Dahlweid M, Moskal M, Santen T, Tobies S, Schulte W (2009) VCC: contract-based modular verification of concurrent C. In: 2009 31st International conference on software engineering-companion volume. IEEE, pp 429-430
[38] de Roever W-P (2001) Concurrency verification: introduction to compositional and non-compositional methods, volume 54 of Cambridge tracts in theoretical computer science. Cambridge University Press, Cambridge
[39] De Wulf M, Doyen L, Henzinger TA, Raskin J-F (2006) Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of CAV. Springer, Berlin, pp 17-30 · Zbl 1188.68171
[40] Ferrari G-L, Degano P, Basile D (2017) Automata for specifying and orchestrating service contracts. In: Logical methods in computer science, volume 12. Episciences.org · Zbl 1398.68296
[41] Filliâtre, J-C; Paskevich, A., Why3-Where programs meet provers, No. 7792, 125-128 (2013), Berlin
[42] Famelis M, Salay R, Chechik M (2012) Partial models: towards modeling and reasoning with uncertainty. In: Proceedings of ICSE’12. IEEE, pp 573-583
[43] Famelis M, Salay R, Chechik M (2012) The semantics of partial model transformations. In: Proceedings of MiSE’12. IEEE, pp 64-69
[44] Famelis M, Salay R, Di Sandro A, Chechik M (2013) Transformation of models containing uncertainty. In: Proceedings of MODELS’13. Springer, Berlin, pp 673-689
[45] Giannakopoulou D, Magee J (2003) Fluent model checking for event-based systems. In: Proceedings of SIGSOFT FSE’03. ACM, pp 257-266
[46] Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of ASE’02. IEEE, pp 3-12
[47] Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. J Autom Softw Eng 12(3), 297-320 (2005)
[48] Giannakopoulou D, Pasareanu CS, Cobleigh JM (2004) Assume-guarantee verification of source code with design-level assumptions. In: Proceedings of ICSE’04. IEEE Computer Society, pp 211-220
[49] Harel, D.: Statecharts: a visual formalism for complex systems. Sci Computer Program 8(3), 231-274 (1987) · Zbl 0637.68010
[50] Harel, D.; Kozen, D.; Tiuryn, J., Dynamic logic, 99-217 (2001), Berlin · Zbl 1003.03528
[51] Hähnle, R.; Schaefer, I.; Tiziana, M. (ed.); Bernhard, S. (ed.), A Liskov principle for delta-oriented programming, 32-46 (2012), Springer, Berlin
[52] Huth M (2002) Model checking modal transition systems using kripke structures. In: Proceedings of VMCAI’02, volume 2294 of LNCS, pp 302-316 · Zbl 1057.68066
[53] Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans Programm Lang Syst (TOPLAS) 5(4), 596-619 (1983) · Zbl 0517.68032
[54] Jonsson, B.: Compositional specification and verification of distributed systems. ACM Trans Program Lang Syst 16(2), 259-303 (1994)
[55] Jacobs, B.; Smans, J.; Philippaerts, P.; Vogels, F.; Penninckx, W.; Piessens, F., VeriFast: a powerful, sound, predictable, fast verifier for C and Java, 41-55 (2011), New York
[56] Keller, R.M.: Formal verification of parallel programs. Commun ACM 19(7), 371-384 (1976) · Zbl 0329.68016
[57] Kupferman, O.; Vardi, M., Synthesis with incomplete information, 109-127 (2000), Berlin · Zbl 0953.68090
[58] Leavens, GT; Baker, AL; Ruby, C., JML: a notation for detailed design, 175-188 (1999), Berlin
[59] Li W, Dworkin L, Seshia SA (2011) Mining assumptions for synthesis. In: Proceedings of ACM/IEEE MEMCODE’11, pp 43-50
[60] Leino, KRM, Dafny: an automatic program verifier for functional correctness, 348-370 (2010), Berlin · Zbl 1253.68095
[61] Levy, L.S.: Taming the tiger: software engineering and software economics. Springer Books on Professional Computing Series, Springer-Verlag, Berlin (1987) · Zbl 0623.68003
[62] Li, X., Fan, Y., Sheng, Q.Z., Maamar, Z., Zhu, H.: A petri net approach to analyzing behavioral compatibility and similarity of web services. IEEE Trans Syst Man Cybern A Syst Hum 41(3), 510-521 (2011)
[63] Lorenzoli D, Mariani L, Pezzè M (2008) Automatic generation of software behavioral models. In: Proceedings of ICSE’08, pp 501-510
[64] Larsen, KG; Steffen, B.; Weise, C., A constraint oriented proof methodology based on modal transition systems, 17-40 (1995), Berlin
[65] Lynch N, Tuttle MR (1987) Hierarchical correctness proofs for distributed algorithms. In: Proceedings of the sixth annual ACM symposium on principles of distributed computing. ACM, pp 137-151
[66] Larsen KG, Thomsen B (1988) A modal process logic. In Proceedings of LICS’88, IEEE, pp 203-210
[67] Lynch, NA; Tuttle, MR, No article title, An introduction to input/outputautomata. CWI Q, 2, 219-246 (1989)
[68] Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. Trans Program Lang Syst (TOPLAS) 16(6), 1811-1841 (1994)
[69] Menghi C, Garcia S, Pelliccione P, Tumova J (2018) Multi-robot LTL planning under uncertainty. In: Proceedings of FM’18
[70] Menghi C, García S, Pelliccione P, Tumova J (2018) Towards multi-robot applications planning under uncertainty. In: Proceedings of ICSE’18, companion proceedings
[71] Magee, J., Kramer, J.: State models and Java programs. Wiley, Hoboken (1999) · Zbl 0924.68026
[72] Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: Proceedings of PODC’90. ACM, pp 377-410
[73] Miller R, Shanahan M (1999) The event calculus in classical logic—alternative axiomatizations. Elect Trans AI 4
[74] Menghi C, Spoletini P, Chechik M, Ghezzi C (2018) Supporting verification-driven incremental distributed design of components. In: Proceedings of FASE’18. Springer, Berlin
[75] Menghi C, Spoletini P, Ghezzi C (2016) Dealing with incompleteness in automata-based model checking. In: Proceedings of FM’16. Springer, Berlin, pp 531-550
[76] Menghi C, Spoletini P, Ghezzi C (2017) Integrating goal model analysis with iterative design. In: Proceedings of REFSQ’17. Springer, Berlin, pp 112-128
[77] Müller, P.; Schwerhoff, M.; Summers, AJ, Viper: a verification infrastructure for permission-based reasoning, 41-62 (2016), Berlin · Zbl 06559851
[78] Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun ACM 15(12), 1053-1058 (1972)
[79] Parnas, D.L.: A technique for software module specification with examples. Commun ACM 15(5), 330-336 (1972)
[80] Pistore M, Barbon F, Bertoli P, Shaparau D, Traverso P (2004) Planning and monitoring Web service composition. In: Proceedings of AIMSA’04, Springer, Berlin, pp 106-115
[81] Pretschner A, Broy M, Kruger IH, Stauner T (2007) Software engineering for automotive systems: a roadmap. In: Proceedings of FOSE’07, IEEE Computer Society, pp 55-71
[82] Pohl, K., Böckle, G., van Der Linden, F.J.: Software product line engineering: foundations, principles and techniques. Springer, Berlin (2005) · Zbl 1075.68575
[83] Pnueli, A.; Krzysztof, RA (ed.), In transition from global to modular temporal reasoning about programs, 123-144 (1985), New York
[84] Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL’89. ACM, pp 179-190 · Zbl 0686.68015
[85] Polikarpova N, Tschannen J, Furia CA (2015) A fully verified container library. In: Formal methods (FM), Lecture Notes in Computer Science. Springer, Berlin
[86] Díaz, RRP; Nores, ML; Pazos, AJJ; Vilas, AF; Duque, JG; Solla, AG; Martínez, BB; Cabrer, MR; Jan, B. (ed.); Charles, K. (ed.), Supporting software variability by reusing generic incomplete models at the requirements specification stage (2004), Berlin
[87] Sandewall, E.: Features and fluents (vol 1): the representation of knowledge about dynamical systems. Oxford University Press, Oxford (1995) · Zbl 0842.68077
[88] Saadatpanah P, Famelis M, Gorzny J, Robinson N, Chechik M, Salay R (2012) Comparing the effectiveness of reasoning formalisms for partial models. In: Proceedings of MoDeVVA’12, ACM, pp 41-46
[89] Solar-Lezama A (2008) Program synthesis by sketching. PhD thesis, University of California, Berkeley
[90] Solar-Lezama, A., No article title, Program sketching. STTT, 15, 475-495 (2013)
[91] Software Measurement Services Ltd (2004) “small project”, “medium-size project”, and “large project”: What do these terms mean? http://www.totalmetrics.com/function-points-downloads/Function-Point-Scale-Project-Size.pdf
[92] Sharifloo, AM; Spoletini, P., Lover: light-weight formal verification of adaptive systems at run time, 170-187 (2013), Berlin
[93] Sibay GE, Uchitel S, Braberman V, Kramer J (2011) Distribution of modal transition systems. In: Proceedings of FM’11, pp 403-417 · Zbl 1372.68188
[94] Beek, MH; Vink, EP; Tiziana, M. (ed.); Bernhard, S. (ed.), Towards modular verification of software product lines with mCRL2, 368-385 (2014), Springer, Berlin
[95] ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J Log Algeb Methods Program 85(2), 287-315 (2016) · Zbl 1351.68170
[96] Beek, MH; Kleijn, J., Team automata satisfying compositionality, 381-400 (2003), Berlin
[97] Ter Beek MH, Mazzanti F (2014) VMC: recent advances and challenges ahead. In: International software product line conference: companion volume for workshops, demonstrations and tools-volume 2. ACM, pp 70-77
[98] Beek, MH; Reniers, MA; Vink, EP; Tiziana, M. (ed.); Bernhard, S. (ed.), Supervisory controller synthesis for product lines using CIF 3, 856-873 (2016), Berlin
[99] Tschannen, J.; Furia, CA; Nordio, M.; Polikarpova, N., AutoProof: auto-active functional verification of object-oriented programs, 566-580 (2015), Berlin
[100] Tabakov D, Vardi MY (2005) Experimental evaluation of classical automata constructions. In: Proceedings of LPAR. Springer, Berlin, pp 396-411 · Zbl 1143.68443
[101] Tabakov D, Vardi MY (2007) Model checking Buchi specifications. In: Proceedings of LATA, pp 565-576
[102] Uchitel, S., Alrajeh, D., Ben-David, S., Braberman, V., Chechik, M., De Caso, G., D’Ippolito, N., Fischbein, D., Garbervetsky, D., Kramer, J., Russo, A., German, S.E.: Supporting incremental behaviour model elaboration. Comput Sci-Res Dev 28(4), 279-293 (2013)
[103] Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3), 384-406 (2009)
[104] Beek, DA; Fokkink, WJ; Hendriks, D.; Hofkamp, A.; Markovski, J.; Mortel-Fronczak, JM; Reniers, MA, CIF 3: model-based engineering of supervisory controllers, 575-580 (2014), Berlin
[105] Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. J Inf Comput 115(1), 1-37 (1994) · Zbl 0827.03009
[106] Yuan, J., Pixley, C., Aziz, A.: Constraint-based verification. Springer, Berlin (2006) · Zbl 1093.68058
[107] Zaremski, A.M., Wing, J.M.: Specification matching of software components. ACM Trans Softw Eng Methodol 6(4), 333-369 (1997)
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.