Nafiseh Kahani
James R. Cordy
ABSTRACT
The automated synthesis of behavioural models in the form of state machines (SMs) from higher-level specifications has a high potential impact on the efficiency and accuracy of software development using models. In this paper, inspired by program synthesis techniques, we propose a model synthesis approach that takes as input a structural model of a system and its desired system properties, and automatically synthesizes executable SMs for its components. To this end, we first generate a synthesis formula for each component, consistent with the system properties, and then perform a State Space Exploration (SSE) of each component, based on its synthesis formula. The result of the SSE is saved in a Labeled Transition System (LTS), for which we then synthesize detailed actions for each of its transitions. Finally, we transform the LTSs into UML-RT (UML real-time profile) SMs, and integrate them with the original structural models. We assess the applicability, performance, and scalability of our approach using several different use cases extracted from the literature.
- K. Czarnecki and S. Helsen, "Classification of model transformation approaches," in Proceedings of the 2nd OOPSLA Workshop on Generative Techniques in the Context of the Model Driven Architecture, vol. 45, no. 3, 2003, pp. 1--17.Google Scholar
- T. Mens and P. Van Gorp, "A taxonomy of model transformation," Electronic Notes in Theoretical Computer Science, vol. 152, pp. 125--142, 2006.Google ScholarDigital Library
- N. Kahani and J. Cordy, "Comparison and evaluation of model transformation tools," in Tech. Rep. 2015--627. Queen's University, Dec. 2015, pp. 1--42.Google Scholar
- N. Kahani, M. Bagherzadeh, J. Cordy, J. Dingel, and D. Varró, "Survey and classification of model transformation tools," Software and Systems Modeling, vol. 18, no. 4, p. 2361--2397, 2019.Google ScholarDigital Library
- B. Selic, "What will it take? a view on adoption of model-based methods in practice," Software and Systems Modeling, vol. 11, no. 4, pp. 513--526, 2012.Google ScholarDigital Library
- D. Harel, H. Kugler, and A. Pnueli, "Synthesis revisited: Generating statechart models from scenario-based requirements," in Formal Methods in Software and Systems Modeling, 2005, pp. 309--324.Google ScholarCross Ref
- S. Uchitel, G. Brunet, and M. Chechik, "Behavior model synthesis from properties and scenarios," in Proc. 29th Intl. Conf. on Software Engineering, 2007, pp. 34--43.Google ScholarDigital Library
- C. Damas, B. Lambeau, P. Dupont, and A. V. Lamsweerde, "Generating annotated behavior models from end-user scenarios," IEEE Trans. on Software Engineering, vol. 31, no. 12, pp. 1056--1073, 2005.Google ScholarDigital Library
- S. Uchitel and J. Kramer, "A workbench for synthesising behaviour models from scenarios," in Proc. 23rd Intl. Conf. on Software engineering, 2001, pp. 188--197.Google ScholarDigital Library
- N. Kahani, "Automodel: a domain-specific language for automatic modeling of real-time embedded systems," in 2018 IEEE/ACM 40th International Conference on Software Engineering: Companion (ICSE-Companion), 2018, pp. 515--517.Google Scholar
- J. Whittle and J. Schumann, "Generating statechart designs from scenarios," in Proc. 22nd Intl. Conf. on Software engineering, 2000, pp. 314--323.Google ScholarDigital Library
- J. Whittle and P. K. Jayaraman, "Synthesizing hierarchical state machines from expressive scenario descriptions," ACM Trans. on Software Engineering and Methodology, vol. 19, no. 3, pp. 1--45, 2010.Google ScholarDigital Library
- R. Rosner, "Modular synthesis of reactive systems," Ph.D. dissertation, 1992.Google Scholar
- E. Letier and W. Heaven, "Requirements modelling by synthesis of deontic input-output automata," in 2013 35th International Conference on Software Engineering (ICSE), 2013, pp. 592--601.Google Scholar
- A. Pnueli and R. Rosner, "On the synthesis of a reactive module," in Proceedings of the 16th Symposium on Principles of Programming Languages, 1989, pp. 179--190.Google Scholar
- S. Maoz, J. O. Ringert, and R. Shalom, "Symbolic repairs for GR(1) specifications," in Proc. 41st Intl. Conf. on Software Engineering, 2019, pp. 1016--1026.Google ScholarDigital Library
- S. Gulwani, O. Polozov, and R. Singh, "Foundations and trends in programming languages," ACM Trans. Comput. Log., vol. 4, no. 1--2, pp. 1--119, 2017.Google Scholar
- S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari, "Oracle-guided component-based program synthesis," in Proc. 32nd Intl. Conf. on Software Engineering, 2010, pp. 215--224.Google Scholar
- R. Joshi, G. Nelson, and K. Randall, "Denali: A goal-directed superoptimizer," in PLDI, 2002, pp. 304--314.Google ScholarDigital Library
- S. Bansal and A. Aiken, "Binary translation using peephole superoptimizers," in Proc. 8th USENIX Conf. on Operating Systems Design and Impl., 2008, pp. 177--192.Google ScholarDigital Library
- B. Selic, "Using UML for modeling complex real-time systems," in Languages, Compilers, and Tools for Embedded Systems, 1998, pp. 250--260.Google Scholar
- Eclipse Foundation, "Eclipse Papyrus for Real Time (Papyrus-RT)," https://www.eclipse.org/papyrus-rt, 2019, retrieved March 19, 2019.Google Scholar
- N. Kahani, N. Hili, J. Cordy, and J. Dingel, "Evaluation of UML-RT and Papyrus-RT for modelling self-adaptive systems," in Proc. 9th Intl. Workshop on Modelling in Software Engineering, 2017, pp. 12--18.Google ScholarDigital Library
- N. Kahani, M. Bagherzadeh, and J. Cordy, "UMLRTSynthesizer," https://github.com/nafisehka/UMLRTSynthesizer, 2020.Google Scholar
- IBM, "IBM RSARTE," 2016, retrieved July 19, 2019. [Online]. Available: https://www.ibm.com/developerworks/downloads/r/architect/index.htmlGoogle Scholar
- C. Damas, B. Lambeau, and A. Van Lamsweerde, "Scenarios, goals, and state machines: a win-win partnership for model synthesis," in Proc. 14th Intl. Symp. on Foundations of Software Engineering, 2006, p. 197--207.Google ScholarDigital Library
- D. Sangiorgi, Introduction to bisimulation and coinduction. Cambridge University Press, 2011.Google ScholarDigital Library
- N. A. Lynch, Distributed algorithms. Elsevier, 1996.Google Scholar
- "Z3," https://github.com/Z3Prover/z3.Google Scholar
- D. S. Kolovos, R. F. Paige, and F. A. Polack, "The Epsilon transformation language," in Intl. Conf. on Theory and Practice of Model Transformations, 2008, pp. 46--60.Google ScholarDigital Library
- Xtext. (2017) Xtext. [Online]. Available: http://www.eclipse.org/Xtext.Google Scholar
- EMF. (2017) Eclipse Modeling Framework (EMF). [Online]. Available: https://www.eclipse.org/modeling/emf.Google Scholar
- S. Uchitel, J. Kramer, and J. Magee, "Synthesis of behavioral models from scenarios," IEEE Trans. on Software Engineering, vol. 29, no. 2, p. 99--115, 2003.Google ScholarDigital Library
- S. Vasilache and J. Tanaka, "Synthesis of state machines from multiple interrelated scenarios using dependency diagrams," in In 8th World Multiconf. on systemics, cybernetics and informatics, 2004, pp. 49--54.Google Scholar
- R. Hennicker and A. Knapp, "Activity-driven synthesis of state machines," in Intl. Conf. on Fundamental Approaches to Software Engineering, 2007, pp. 87--101.Google ScholarCross Ref
- A. Ali, D. Jawawi, and M. A. Isa, "Scalable scenario specifications to synthesize component-centric behaviour models," Intl. Journal of Software Engineering and Its Applications, vol. 9, no. 9, pp. 79--106, 2015.Google ScholarCross Ref
- I. Krka, Y. Brun, G. Edwards, and N. Medvidovic, "Synthesizing partial component-level behavior models from system specifications," in Proc. 7th Joint Meeting on Foundations of Software Engineering, 2009, pp. 305--314.Google Scholar
- N. Kahani, "Synthesis and verification of models using satisfiability modulo theories," Ph.D. dissertation, 2020.Google Scholar
- D. Harel, "Statecharts: A visual formalism for complex systems," Science of Computer Programming, vol. 8, no. 3, pp. 231--274, 1987.Google ScholarDigital Library
- I. Beschastnikh, Y. Brun, M. D. Ernst, and A. Krishnamurthy, "Inferring models of concurrent systems from logs of their behavior with CSight," in Proc. 36th Intl. Conf. on Software Engineering, 2014, pp. 468--479.Google Scholar
- I. Buzhinsky and V. Vyatkin, "Automatic inference of finite-state plant models from traces and temporal properties," IEEE Trans. on Industrial Informatics, vol. 13, no. 4, pp. 1521--1530, 2017.Google ScholarCross Ref
- N. Walkinshaw, R. Taylor, and J. Derrick, "Inferring extended finite state machine models from software executions," Empirical Software Engineering, vol. 21, no. 3, pp. 811--853, 2016.Google ScholarDigital Library
- I. Krüger, R. Grosu, P. Scholz, and M. Broy, "From MSCs to statecharts," in Intl. Workshop on Distributed and Parallel Embedded Systems (DIPES'98), 1999, p. 61--71.Google ScholarCross Ref
- D. Harel and H. Kugler, "Synthesizing state-based object systems from LSC specifications," Intl. J. of Foundations of Computer Science, vol. 13, no. 1, pp. 5--51, 2002.Google ScholarCross Ref
- F. Vaandrager, "Model learning," Communications of the ACM, vol. 60, no. 2, pp. 86--95, 2017.Google ScholarDigital Library
- D. Dill, "Trace theory for automatic hierarchical verification of speed independent circuits," MA: MIT press, vol. 24, pp. 1--180, 1989.Google Scholar
- R. Alur and S. L. Torre, "Deterministic generators and games for LTL fragments," ACM Trans. Comput. Log., vol. 5, no. 1, pp. 1--25, 2004.Google ScholarDigital Library
- N. P. O. Kupferman and M. Vardi, "Safraless compositional synthesis," in Computer Aided Verification (CAV), 2006, pp. 31--44.Google Scholar
- Y. Diaz-Mercado, A. Jones, C. Belta, and M. Egerstedt, "Correct-by-construction control synthesis for multi-robot mixing," in 54th IEEE Conf. on Decision and Control (CDC), 2015, pp. 221--226.Google Scholar
- H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas, "Temporal-logic-based reactive mission and motion planning," IEEE Transactions on Robotics, vol. 25, no. 6, pp. 1370--1381, 2009.Google ScholarDigital Library
- R. Alur, S. Moarref, and U. Topcu, "Compositional and symbolic synthesis of reactive controllers for multi-agent systems," in Information and Computation, 2018, pp. 616--633.Google ScholarCross Ref
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan, "Synthesis of loop-free programs," in PLDI, 2011, pp. 62--73.Google Scholar
- A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat, "Combinatorial sketching for finite programs," ACM SIGPLAN Notices, vol. 49, no. 11, pp. 404--415, 2006.Google ScholarDigital Library
- E. Kneuss, I. Kuraj, V. Kuncak, and P. Suter, "Synthesis modulo recursive functions," ACM SIGPLAN Notices, vol. 48, no. 10, pp. 407--426, 2013.Google ScholarDigital Library
- A. Reynolds, M. Deters, V. Kuncak, C. Tinelli, and C. Barrett, "Counterexample-guided quantifier instantiation for synthesis in SMT," in Intl. Conf. on Computer Aided Verification, 2015, pp. 198--216.Google ScholarCross Ref
- Z. Huang, Y. Wang, S. Mitra, G. E. Dullerud, and S. Chaudhuri, "Controller synthesis with inductive proofs for piecewise linear systems: An SMT-based algorithm," in 54th IEEE Conf. on decision and control (CDC), 2015, pp. 7434--7439.Google Scholar
- S. Srivastava, S. Gulwani, and J. S. Foster, "From program verification to program synthesis," in ACM Sigplan Notices, vol. 45, no. 1, 2010, pp. 313--326.Google ScholarDigital Library
- S. Itzhaky, S. Gulwani, N. Immerman, and M. Sagiv, "A simple inductive synthesis methodology and its applications," in ACM Sigplan Notices, vol. 45, no. 10, 2010, pp. 36--46.Google ScholarDigital Library
- A. Albarghouthi, S. Gulwani, and Z. Kincaid, "Recursive program synthesis," in Intl. Conf. on computer aided verification, 2013, pp. 934--950.Google ScholarCross Ref
- A. Solar-Lezama, "The sketching approach to program synthesis," in Asian Symp. on Programming Languages and Systems, 2009, pp. 4--13.Google Scholar
- M. Bagherzadeh, N. Kahani, J. Karim, and J. Dingel, "PMExec: An execution engine of partial UML-RT models," in 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2019, pp. 1178--1181.Google Scholar
- M. Bagherzadeh, N. Kahani, J. Karim, and J. Dingel, "Execution of partial state machine models," IEEE Transactions on Software Engineering (TSE), pp. 1--27, July 2020.Google ScholarCross Ref
Index Terms
- Synthesis of state machine models
Recommendations
Papyrus: a UML2 tool for domain-specific language modeling
MBEERTS'07: Proceedings of the 2007 International Dagstuhl conference on Model-based engineering of embedded real-time systemsThis chapter outlines Papyrus, a tool for graphical modeling of UML2 applications. It is an open-source project, designed as an Eclipse component, and based on the existing EMF-based realization of the UML2 meta-model. The goal of this open-source ...
Model-level, platform-independent debugging in the context of the model-driven development of real-time systems
ESEC/FSE 2017: Proceedings of the 2017 11th Joint Meeting on Foundations of Software EngineeringProviding proper support for debugging models at model-level is one of the main barriers to a broader adoption of Model Driven Development (MDD). In this paper, we focus on the use of MDD for the development of real-time embedded systems (RTE). We ...
MDebugger: a model-level debugger for UML-RT
ICSE '18: Proceedings of the 40th International Conference on Software Engineering: Companion ProceeedingsIdeally, debuggers for Model-Driven Development (MDD) tools would allow users to 'stay at the model-level' and would not require them to refer to the generated source code or figure out how the code generator works. Existing approaches to model-level ...
Comments