[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) · doi:10.1023/A:1008739929481 |
[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) · doi:10.1145/291252.288305 |
[9] |
Alur, R., Yannakakis, M.: Model checking of hierarchical state machines. ACM Trans Program Lang Syst (TOPLAS) 23(3), 273-303 (2001) · doi:10.1145/503502.503503 |
[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) · doi:10.1016/j.entcs.2008.06.022 |
[12] |
Blom, S.; Darabi, S.; Huisman, M., Verification of loop parallelisations, 202-217 (2015), Berlin · doi:10.1007/978-3-662-46675-9_14 |
[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) · doi:10.1007/s10009-013-0293-y |
[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 · doi:10.1007/s10703-008-0053-x |
[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 · doi:10.1145/990010.990011 |
[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 · doi:10.1016/j.tcs.2013.03.006 |
[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 · doi:10.1007/978-3-642-20398-5_35 |
[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) · doi:10.1016/j.scico.2014.06.011 |
[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 · Zbl 1009.68020 |
[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 · Zbl 1435.68366 |
[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) · doi:10.1007/s10515-005-2641-y |
[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 · doi:10.1016/0167-6423(87)90035-9 |
[50] |
Harel, D.; Kozen, D.; Tiuryn, J., Dynamic logic, 99-217 (2001), Berlin · Zbl 1003.03528 · doi:10.1007/978-94-017-0456-4_2 |
[51] |
Hähnle, R.; Schaefer, I.; Tiziana, M. (ed.); Bernhard, S. (ed.), A Liskov principle for delta-oriented programming, 32-46 (2012), Springer, Berlin · doi:10.1007/978-3-642-34781-8 |
[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 · doi:10.1145/69575.69577 |
[54] |
Jonsson, B.: Compositional specification and verification of distributed systems. ACM Trans Program Lang Syst 16(2), 259-303 (1994) · doi:10.1145/174662.174665 |
[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 · doi:10.1007/978-3-642-20398-5_4 |
[56] |
Keller, R.M.: Formal verification of parallel programs. Commun ACM 19(7), 371-384 (1976) · Zbl 0329.68016 · doi:10.1145/360248.360251 |
[57] |
Kupferman, O.; Vardi, M., Synthesis with incomplete information, 109-127 (2000), Berlin · Zbl 0953.68090 · doi:10.1007/978-94-015-9586-5_6 |
[58] |
Leavens, GT; Baker, AL; Ruby, C., JML: a notation for detailed design, 175-188 (1999), Berlin · doi:10.1007/978-1-4615-5229-1_12 |
[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 · doi:10.1007/978-3-642-17511-4_20 |
[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 · doi:10.1007/978-1-4612-4718-0 |
[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) · doi:10.1109/TSMCA.2010.2093884 |
[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) · Zbl 0677.68067 |
[68] |
Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. Trans Program Lang Syst (TOPLAS) 16(6), 1811-1841 (1994) · doi:10.1145/197320.197383 |
[69] |
Menghi C, Garcia S, Pelliccione P, Tumova J (2018) Multi-robot LTL planning under uncertainty. In: Proceedings of FM’18 · Zbl 1460.68119 |
[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 · Zbl 1460.68119 |
[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 · Zbl 1425.68261 |
[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 · Zbl 1427.68170 |
[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 1475.68191 · doi:10.1007/978-3-662-49122-5_2 |
[78] |
Parnas, D.L.: On the criteria to be used in decomposing systems into modules. Commun ACM 15(12), 1053-1058 (1972) · doi:10.1145/361598.361623 |
[79] |
Parnas, D.L.: A technique for software module specification with examples. Commun ACM 15(5), 330-336 (1972) · doi:10.1145/355602.361309 |
[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 · doi:10.1007/3-540-28901-1 |
[83] |
Pnueli, A.; Krzysztof, RA (ed.), In transition from global to modular temporal reasoning about programs, 123-144 (1985), New York · Zbl 0578.68014 · doi:10.1007/978-3-642-82453-1_5 |
[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 · doi:10.1007/978-3-642-35861-6_11 |
[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 · doi:10.1016/j.jlamp.2015.11.006 |
[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 · doi:10.1007/978-3-319-47166-2_59 |
[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) · doi:10.1007/s00450-012-0233-1 |
[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) · doi:10.1109/TSE.2008.107 |
[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 · doi:10.1007/978-3-642-54862-8_48 |
[105] |
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. J Inf Comput 115(1), 1-37 (1994) · Zbl 0827.03009 · doi:10.1006/inco.1994.1092 |
[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) · doi:10.1145/261640.261641 |