Formal Aspects of Computing

, Volume 31, Issue 5, pp 459–502 | Cite as

A verification-driven framework for iterative design of controllers

  • Claudio MenghiEmail author
  • Paola Spoletini
  • Marsha Chechik
  • Carlo Ghezzi
Open Access
Original Article


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.


Distributed development Controller design Verification-driven development 



This work has received funding from the European Research Council under the EUs Horizon 2020 research and innovation programme (grant agreement No 731869 and No 694277).

We would like to thank the reviewers of FASE’18 for their insightful comments and Dimitra Giannakopoulou for her help with the Mars Rover case study.


  1. ABKS16.
    Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-oriented software product lines. Springer, Berlin (2016)Google Scholar
  2. AFFM06.
    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–385Google Scholar
  3. AFT08.
    Amalfitano D, Fasolino AR, Tramontana P (2008) Reverse engineering finite state machines from rich Internet applications. In: Proceedings of WCRE'08, pp 69–73Google Scholar
  4. AH99.
    Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Softw Des 15(1), 7–48 (1999)CrossRefGoogle Scholar
  5. AMT13.
    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–33Google Scholar
  6. AMT15.
    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–516Google Scholar
  7. AMT16.
    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–269Google Scholar
  8. AY98.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM SIGSOFT Softw Eng Notes 23(6), 175–188 (1998)CrossRefGoogle Scholar
  9. AY01.
    Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans Program Lang Syst (TOPLAS) 23(3), 273–303 (2001)CrossRefGoogle Scholar
  10. BBKT04.
    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–43Google Scholar
  11. BD08.
    Belguidoum, M., Dagnat, F.: Formalization of component substitutability. Electron Notes Theor Comput Sci 215, 75–92 (2008)CrossRefGoogle Scholar
  12. BDH15.
    Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. International conference on fundamental approaches to software engineering, pp. 202–217. Springer, Berlin (2015)CrossRefGoogle Scholar
  13. BG99.
    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–287Google Scholar
  14. BMS+17.
    Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. Proceeding of SEFM'17, pp. 54–69. Springer, Berlin (2017)Google Scholar
  15. BMU15.
    Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. Softw Tools Technol Transf 17(6), 729–744 (2015)CrossRefGoogle Scholar
  16. Büc90.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. The collected works of J, pp. 425–435. Richard Büchi. Springer, Berlin (1990)Google Scholar
  17. CBDU16.
    Ciolek D, Braberman VA, D'Ippolito N, Uchitel S (2016) Technical report: directed controller synthesis of discrete event systems. arXiv:1605.09772
  18. CBFU06.
    Chechik M, Brunet G, Fischbein D, Uchitel S (2006) Partial behavioural models for requirements and early design. In: Proceedings of Dagstuhl seminar MMOSS, p 6351Google Scholar
  19. CCG+02.
    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–364Google Scholar
  20. CCSS08.
    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)zbMATHCrossRefGoogle Scholar
  21. CDEG03.
    Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans Softw Eng Methodol (TOSEM) 12(4), 371–408 (2003)zbMATHCrossRefGoogle Scholar
  22. CDGV02.
    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–602Google Scholar
  23. CGP99.
    Clarke, E.M.: Orna Grumberg, and Doron Peled. MIT Press, Cambridge, Model checking (1999)Google Scholar
  24. CGP03.
    Cobleigh JM, Giannakopoulou D, Păsăreanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of TACAS'03. Springer, Berlin, pp 331–346Google Scholar
  25. CH01.
    Councill, W.T., Heineman, G.T.: Component-based software engineering: putting the pieces together, pp. 5–99. Addison Wesley, New York (2001)Google Scholar
  26. CK13.
    Carmona, J., Kleijn, J.: Compatibility in a multi-component environment. Theor Comput Sci 484, 1–15 (2013)MathSciNetzbMATHCrossRefGoogle Scholar
  27. LKF02.
    Li HC, Krishnamurthi S, Fisler K (2002) Interfaces for modular feature verification. In: Proceedings 17th IEEE international conference on automated software engineering, pp 195–204Google Scholar
  28. Cok11.
    Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. NASA formal methods symposium, pp. 472–479. Springer, Berlin (2011)CrossRefGoogle Scholar
  29. CPRT15.
    Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong and strong ycling Planning via symbolic model checking. Technical report, IRST (2015)zbMATHGoogle Scholar
  30. CT15.
    Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci Comput Programming 97, 333–348 (2015)CrossRefGoogle Scholar
  31. DAC98.
    Dwyer MB, Avrunin GS, Corbett JC (1998) Property Specification patterns for finite-state verification. In: Proceedings of FMSP'98. ACM, pp 7–15Google Scholar
  32. dAH01.
    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–120Google Scholar
  33. DBPU10.
    D'Ippolito N, Braberman V, Piterman N, Uchitel S (2010) Synthesis of live behaviour models. In: Proceedings of SIGSOFT FSE'10. ACM, pp 77–86Google Scholar
  34. DBPU11.
    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–220Google Scholar
  35. DBPU13.
    D'Ippolito N, Braberman V, Piterman N, Uchitel S (2013) Synthesising non-anomalous event-based controllers for liveness goals. ACM Trans Softw Eng Methodol 22Google Scholar
  36. DGV13.
    De Giacomo G, Vardi MY (2013) Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of IJCAI. ACM, pp 854–860Google Scholar
  37. DMS+09.
    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–430Google Scholar
  38. dR01.
    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, CambridgeGoogle Scholar
  39. DWDHR06.
    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–30Google Scholar
  40. FDB17.
    Ferrari G-L, Degano P, Basile D (2017) Automata for specifying and orchestrating service contracts. In: Logical methods in computer science, volume 12. Episciences.orgGoogle Scholar
  41. FP13.
    Filliâtre, J.-C., Paskevich, A.: Why3–Where programs meet provers. European symposium on programming. Lecture Notes in Computer Science, vol. 7792, pp. 125–128. Springer, Berlin (2013)Google Scholar
  42. FSC12a.
    Famelis M, Salay R, Chechik M (2012) Partial models: towards modeling and reasoning with uncertainty. In: Proceedings of ICSE'12. IEEE, pp 573–583Google Scholar
  43. FSC12b.
    Famelis M, Salay R, Chechik M (2012) The semantics of partial model transformations. In: Proceedings of MiSE'12. IEEE, pp 64–69Google Scholar
  44. FSDSC13.
    Famelis M, Salay R, Di Sandro A, Chechik M (2013) Transformation of models containing uncertainty. In: Proceedings of MODELS'13. Springer, Berlin, pp 673–689Google Scholar
  45. GM03.
    Giannakopoulou D, Magee J (2003) Fluent model checking for event-based systems. In: Proceedings of SIGSOFT FSE'03. ACM, pp 257–266Google Scholar
  46. GPB02.
    Giannakopoulou D, Pasareanu CS, Barringer H (2002) Assumption generation for software component verification. In: Proceedings of ASE'02. IEEE, pp 3–12Google Scholar
  47. GPB05.
    Giannakopoulou, D., Păsăreanu, C.S., Barringer, H.: Component verification with automatically generated assumptions. J Autom Softw Eng 12(3), 297–320 (2005)CrossRefGoogle Scholar
  48. GPC04.
    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–220Google Scholar
  49. Har87.
    Harel, D.: Statecharts: a visual formalism for complex systems. Sci Computer Program 8(3), 231–274 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
  50. HKT01.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. Handbook of philosophical logic, pp. 99–217. Springer, Berlin (2001)zbMATHCrossRefGoogle Scholar
  51. HS12.
    Hähnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Tiziana, M., Bernhard, S. (eds) Leveraging applications of formal methods, verification and validation, pp. 32–46. Technologies for mastering change, Springer, Berlin (2012)CrossRefGoogle Scholar
  52. Hut02.
    Huth M (2002) Model checking modal transition systems using kripke structures. In: Proceedings of VMCAI'02, volume 2294 of LNCS, pp 302–316Google Scholar
  53. Jon83.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans Programm Lang Syst (TOPLAS) 5(4), 596–619 (1983)zbMATHCrossRefGoogle Scholar
  54. Jon94.
    Jonsson, B.: Compositional specification and verification of distributed systems. ACM Trans Program Lang Syst 16(2), 259–303 (1994)CrossRefGoogle Scholar
  55. JSP+11.
    Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. NASA formal methods symposium, pp. 41–55. Springer, New York (2011)CrossRefGoogle Scholar
  56. Kel76.
    Keller, R.M.: Formal verification of parallel programs. Commun ACM 19(7), 371–384 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  57. KV00.
    Kupferman, O., Vardi, M.: Synthesis with incomplete information. Advances in temporal logic, pp. 109–127. Springer, Berlin (2000)CrossRefGoogle Scholar
  58. LBR99.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. Behavioral specifications of businesses and systems, pp. 175–188. Springer, Berlin (1999)CrossRefGoogle Scholar
  59. LDS11.
    Li W, Dworkin L, Seshia SA (2011) Mining assumptions for synthesis. In: Proceedings of ACM/IEEE MEMCODE'11, pp 43–50Google Scholar
  60. Lei10.
    Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. International conference on logic for programming artificial intelligence and reasoning, pp. 348–370. Springer, Berlin (2010)CrossRefGoogle Scholar
  61. Lev87.
    Levy, L.S.: Taming the tiger: software engineering and software economics. Springer Books on Professional Computing Series, Springer-Verlag, Berlin (1987)zbMATHCrossRefGoogle Scholar
  62. LFS+11.
    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)CrossRefGoogle Scholar
  63. LMP08.
    Lorenzoli D, Mariani L, Pezzè M (2008) Automatic generation of software behavioral models. In: Proceedings of ICSE'08, pp 501–510Google Scholar
  64. LSW95.
    Larsen, K.G., Steffen, B., Weise, C.: A constraint oriented proof methodology based on modal transition systems. BRICS notes, pp. 17–40. Springer, Berlin (1995)Google Scholar
  65. LT87.
    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–151Google Scholar
  66. LT88.
    Larsen KG, Thomsen B (1988) A modal process logic. In Proceedings of LICS'88, IEEE, pp 203–210Google Scholar
  67. LT89.
    Lynch, N.A., Tuttle, M.R.: An introduction to input/outputautomata. CWI Q 2, 219–246 (1989)Google Scholar
  68. LW94.
    Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. Trans Program Lang Syst (TOPLAS) 16(6), 1811–1841 (1994)CrossRefGoogle Scholar
  69. MGPT18a.
    Menghi C, Garcia S, Pelliccione P, Tumova J (2018) Multi-robot LTL planning under uncertainty. In: Proceedings of FM'18Google Scholar
  70. MGPT18b.
    Menghi C, García S, Pelliccione P, Tumova J (2018) Towards multi-robot applications planning under uncertainty. In: Proceedings of ICSE'18, companion proceedingsGoogle Scholar
  71. MK99.
    Magee, J., Kramer, J.: State models and Java programs. Wiley, Hoboken (1999)zbMATHGoogle Scholar
  72. MP90.
    Manna Z, Pnueli A (1990) A hierarchy of temporal properties. In: Proceedings of PODC'90. ACM, pp 377–410Google Scholar
  73. MS99.
    Miller R, Shanahan M (1999) The event calculus in classical logic—alternative axiomatizations. Elect Trans AI 4Google Scholar
  74. MSCG18.
    Menghi C, Spoletini P, Chechik M, Ghezzi C (2018) Supporting verification-driven incremental distributed design of components. In: Proceedings of FASE'18. Springer, BerlinGoogle Scholar
  75. MSG16.
    Menghi C, Spoletini P, Ghezzi C (2016) Dealing with incompleteness in automata-based model checking. In: Proceedings of FM'16. Springer, Berlin, pp 531–550Google Scholar
  76. MSG17.
    Menghi C, Spoletini P, Ghezzi C (2017) Integrating goal model analysis with iterative design. In: Proceedings of REFSQ'17. Springer, Berlin, pp 112–128Google Scholar
  77. MSS16.
    Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. International conference on verification, model checking, and abstract interpretation, pp. 41–62. Springer, Berlin (2016)zbMATHCrossRefGoogle Scholar
  78. Par72a.
    Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun ACM 15(12), 1053–1058 (1972)CrossRefGoogle Scholar
  79. Par72b.
    Parnas, D.L.: A technique for software module specification with examples. Commun ACM 15(5), 330–336 (1972)CrossRefGoogle Scholar
  80. PBB+04.
    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–115Google Scholar
  81. PBKS07.
    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–71Google Scholar
  82. PBvDL05.
    Pohl, K., Böckle, G., van Der Linden, F.J.: Software product line engineering: foundations, principles and techniques. Springer, Berlin (2005)zbMATHCrossRefGoogle Scholar
  83. Pnu85.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Krzysztof, R.A. (ed.) Logics and models of concurrent systems, pp. 123–144. Springer, New York (1985)CrossRefGoogle Scholar
  84. PR89.
    Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of POPL'89. ACM, pp 179–190Google Scholar
  85. PTF15.
    Polikarpova N, Tschannen J, Furia CA (2015) A fully verified container library. In: Formal methods (FM), Lecture Notes in Computer Science. Springer, BerlinGoogle Scholar
  86. RNA+04.
    Díaz, R.R.P., Nores, M.L., Pazos, A.J.J., Vilas, A.F., Duque, J.G., Solla, A.G., Martínez, B.B., Cabrer, M.R.: Supporting software variability by reusing generic incomplete models at the requirements specification stage. In: Jan, B., Charles, K. (eds.) Software reuse: methods, techniques, and tools. Springer, Berlin (2004)Google Scholar
  87. San95.
    Sandewall, E.: Features and fluents (vol 1): the representation of knowledge about dynamical systems. Oxford University Press, Oxford (1995)zbMATHGoogle Scholar
  88. SFG+12.
    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–46Google Scholar
  89. SL08.
    Solar-Lezama A (2008) Program synthesis by sketching. PhD thesis, University of California, BerkeleyGoogle Scholar
  90. SL13.
    Solar-Lezama, A.: Program sketching. STTT 15(5), 475–495 (2013)Google Scholar
  91. Sof04.
    Software Measurement Services Ltd (2004) ``small project'', ``medium-size project'', and ``large project'': What do these terms mean?
  92. SS13.
    Sharifloo, A.M., Spoletini, P.: Lover: light-weight formal verification of adaptive systems at run time. Formal aspects of component software, pp. 170–187. Springer, Berlin (2013)CrossRefGoogle Scholar
  93. SUBK11.
    Sibay GE, Uchitel S, Braberman V, Kramer J (2011) Distribution of modal transition systems. In: Proceedings of FM'11, pp 403–417Google Scholar
  94. tBdV14.
    ter Beek, M.H., de Vink, E.P.: Towards modular verification of software product lines with mCRL2. In: Tiziana, M., Bernhard, S. (eds.) Leveraging applications of formal methods, verification and validation, pp. 368–385. Technologies for Mastering Change, Springer, Berlin (2014)Google Scholar
  95. tBFGM16.
    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)MathSciNetzbMATHCrossRefGoogle Scholar
  96. tBK03.
    ter Beek, M.H., Kleijn, J.: Team automata satisfying compositionality. Formal methods (FM), pp. 381–400. Springer, Berlin (2003)Google Scholar
  97. TBM14.
    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–77Google Scholar
  98. tBRdV16.
    ter Beek, M.H., Reniers, M.A., de Vink, E.P.: Supervisory controller synthesis for product lines using CIF 3. In: Tiziana, M., Bernhard, S. (eds.) Leveraging applications of formal methods, verification and validation: foundational techniques, pp. 856–873. Springer, Berlin (2016)CrossRefGoogle Scholar
  99. TFNP15.
    Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. International conference on tools and algorithms for the construction and analysis of systems, pp. 566–580. Lecture Notes in Computer Science. Springer, Berlin (2015)Google Scholar
  100. TV05.
    Tabakov D, Vardi MY (2005) Experimental evaluation of classical automata constructions. In: Proceedings of LPAR. Springer, Berlin, pp 396–411Google Scholar
  101. TV07.
    Tabakov D, Vardi MY (2007) Model checking Buchi specifications. In: Proceedings of LATA, pp 565–576Google Scholar
  102. UABD+13.
    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)CrossRefGoogle Scholar
  103. UBC09.
    Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans Softw Eng 35(3), 384–406 (2009)CrossRefGoogle Scholar
  104. vBFH+14.
    van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: model-based engineering of supervisory controllers. Tools and algorithms for the construction and analysis of systems, pp. 575–580. Springer, Berlin (2014)CrossRefGoogle Scholar
  105. VW94.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. J Inf Comput 115(1), 1–37 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  106. YPA06.
    Yuan, J., Pixley, C., Aziz, A.: Constraint-based verification. Springer, Berlin (2006)zbMATHGoogle Scholar
  107. ZW97.
    Zaremski, A.M., Wing, J.M.: Specification matching of software components. ACM Trans Softw Eng Methodol 6(4), 333–369 (1997)CrossRefGoogle Scholar

Copyright information

© The Author(s) 2019

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (, which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.University of LuxembourgLuxembourgLuxembourg
  2. 2.Kennesaw State UniversityMariettaUSA
  3. 3.University of TorontoTorontoCanada
  4. 4.Politecnico di MilanoMilanItaly

Personalised recommendations