Open and Branching Behavioral Synthesis with Scenario Clauses
DOI:
https://doi.org/10.19153/cleiej.24.3.1Keywords:
Open Systems, Branching Reasoning, Behavioral Specifications, SynthesisAbstract
The Software Engineering community has identified behavioral specification as one of the main challenges to be addressed for the transference of formal verification techniques such as model checking. In particular, expressivity of the specification language is a key factor, especially when dealing with Open Systems and controllability of events and branching time behavior reasoning. In this work, we propose the Feather Weight Visual Scenarios (FVS) language as an appealing declarative and formal verification tool to specify and synthesize the expected behavior of systems. FVS can express linear and branching properties in closed and Open systems. The validity of our approach is proved by employing FVS in complex, complete, and industrial relevant case studies, showing the flexibility and expressive power of FVS, which constitute the crucial features that distinguish our approach.
References
R. Alur, T. Feder, and T. A. Henzinger. The bene ts of relaxing punctuality. Journal of the ACM
(JACM), 43(1):116{146, 1996.
F. Asteasuain and V. Braberman. Speci cation patterns: formal and easy. International Journal of
Software Engineering and Knowledge Engineering, 25(04):669-700, 2015,
F. Asteasuain and V. Braberman. Declaratively building behavior by means of scenario clauses. Require-
ments Engineering, 22(2):239{274, 2017.
F. Asteasuain, F. Calonge, F. Diaz, F. Dangiolo, and P. Gamboa. Expressing early behavior specifi cations
with branching visual scenarios. In CONAIISI, Argentina, ISSN 2347-0372, 2018.
F. Asteasuain, F. Calonge, and M. Dubinsky. Exploring speci fication pattern based behavioral synthesis
with scenario clauses. In 2018 CACIC ISBN 978-950-658-472-6, pages 22,34. CACIC, Argentina, 2018.
F. Asteasuain and F. Tarulla. Exploring architectural model checking with declarative speci cations. In
CACIC, 2017.
A. Bauer, M. Leucker, and C. Schallhart. Monitoring of real-time properties. In International Conference
on Foundations of Software Technology and Theoretical Computer Science, pages 260-272. Springer, 2006.
S. Ben-David and A. Orni. Property-by-example guide: a handbook of psl/sugar examples. PROSYD
deliverable D, 1(3), 2005.
R. Bloem, R. Cavada, C. Esiner, I. Pill, M. Roveri, and S. Semprini. Manual for property simulation and
assurance tool. Technical report, Technical Report Deliverable, 2005.
R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa'Ar. Synthesis of reactive (1) designs. 2011.
A. Bouajjani, Y. Lakhnech, and S. Yovine. Model checking for extended timed temporal logics. In
International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, pages 306-
Springer, 1996.
E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT press, 1999.
B. d'Angelo, S. Sankaranarayanan, C. Sanchez, W. Robinson, B. Finkbeiner, H. B. Sipma, S. Mehrotra,
and Z. Manna. Lola: Runtime monitoring of synchronous systems. In 12th International Symposium on
Temporal Representation and Reasoning (TIME'05), pages 166-174. IEEE, 2005.
L. K. Dillon, G. Kutty, L. E. Moser, P. M. Melliar-Smith, and Y. S. Ramakrishna. A graphical interval
logic for specifying concurrent systems. ACM Transactions on Software Engineering and Methodology
(TOSEM), 3(2):131-165, 1994.
N. DIppolito, V. Braberman, N. Piterman, and S. Uchitel. Synthesising non-anomalous event-based
controllers for liveness goals. ACM Tran, 22(9), 2013.
M. Dwyer, M. Avrunin, and M. Corbett. Patterns in property speci cations for fi nite-state veri fication.
In ICSE, pages 411-420, 1999.
C. Eisner and D. Fisman. A practical introduction to PSL. Springer Science & Business Media, 2007.
O. Friedmann and M. Lange. Solving parity games in practice. In International Symposium on Auto-
mated Technology for Veri cation and Analysis, pages 182-196. Springer, 2009.
P. Gammie and R. Van Der Meyden. Mck: Model checking the logic of knowledge. In International
Conference on Computer Aided Veri cation, pages 479-483. Springer, 2004.
D. Giannakopoulou and J. Magee. Fluent model checking for event-based systems. In ACM SIGSOFT,
volume 28, pages 257-266. ACM, 2003.
I. Grobelna, R. Wisniewski, M. Grobelny, and M. Wisniewska. Design and veri cation of real-life
processes with application of petri nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems,
(11):2856-2869, 2016.
D. Harel. Statecharts: A visual formalism for complex systems. Science of computer programming,
(3):231-274, 1987.
IEEE-Commission et al. Ieee standard for property speci cation language (psl). IEEE Std 1850-2005,
M. Jurdzinski. Small progress measures for solving parity games. In Annual Symposium on Theoretical
Aspects of Computer Science, pages 290-301. Springer, 2000.
R. Koymans. Specifying real-time properties with metric temporal logic. Real-time systems, 2(4):255{
, 1990.
I. Krka, Y. Brun, G. Edwards, and N. Medvidovic. Synthesizing partial component-level behavior
models from system speci cations. In ESEC-FSE.
A. V. Lamsweerde. Goal-oriented requirements engineering: A guided tour. In RE, 2001.
A. Lomuscio, C. Pecheur, and F. Raimondi. Automatic veri cation of knowledge and time with nusmv.
In Proceedings of the Twentieth International Joint Conference on Arti cial Intelligence, pages 1384-
IJCAI/AAAI Press, 2007.
O. Maler and D. Nickovic. Monitoring properties of analog and mixed-signal circuits. International
Journal on Software Tools for Technology Transfer, 15(3):247-268, 2013.
S. Maoz and J. O. Ringert. Synthesizing a lego forklift controller in gr (1): a case study. arXiv preprint
arXiv:1602.01172, 2016.
S. Maoz and Y. Saar. Assume-guarantee scenarios: Semantics and synthesis. In MODELS, pages
-351. Springer, 2012.
M. Mazo, A. Davitian, and P. Tabuada. Pessoa: A tool for embedded controller synthesis. In Interna-
tional Conference on Computer Aided Veri cation, pages 566-569. Springer, 2010.
P. Pelliccione, P. Inverardi, and H. Muccini. Charmy: A framework for designing and verifying architectural
speci cations. IEEE TSE, 35(3):325{346, 2009.
V. Raman, N. Piterman, and H. Kress-Gazit. Provably correct continuous control for high-level robot
behaviors with actions of arbitrary execution durations. In 2013 IEEE International Conference on
Robotics and Automation, pages 4075-4081. IEEE, 2013.
S. Schewe. Solving parity games in big steps. In International Conference on Foundations of Software
Technology and Theoretical Computer Science, pages 449-460. Springer, 2007.
G. E. Sibay, S. Uchitel, V. Braberman, and J. Kramer. Distribution of modal transition systems. In
International Symposium on Formal Methods, pages 403-417. Springer, 2012.
M. H. Smith, G. J. Holzmann, and K. Etessami. Events and constraints: A graphical editor for capturing
logic requirements of programs. In Re.
Y.-K. Tsay, Y.-F. Chen, M.-H. Tsai, K.-N. Wu, and W.-C. Chan. Goal: A graphical tool for manipulating
buchi automata and temporal formulae. In TACAS, pages 466-471. Springer, 2007.
M. Y. Vardi. Branching vs. linear time: Final showdown. In International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, pages 1-22. Springer, 2001.
M. Y. Vardi and P. Wolper. Reasoning about in nite computations. Information and computation,
(1):1-37, 1994.
W. Zielonka. In nite games on nitely coloured graphs with applications to automata on in nite trees.
Theoretical Computer Science, 200(1-2):135-183, 1998.
G. Amram, S. Maoz, and O. Pistiner. Gr (1)*: Gr (1) speci cations extended with existential guarantees.
In International Symposium on Formal Methods, pages 83-100. Springer, 2019.
D. Fahland, D. Lo, and S. Maoz. Mining branching-time scenarios. In 2013 28th IEEE/ACM Interna-
tional Conference on Automated Software Engineering (ASE), pages 443-453. IEEE, 2013.
E. Firman, S. Maoz, and J. O. Ringert. Performance heuristics for gr (1) synthesis and related algorithms.
Acta Informatica, 57(1):37-79, 2020.
S. Maoz and J. O. Ringert. Gr (1) synthesis for ltl speci cation patterns. In Proceedings of the 2015
th Joint Meeting on Foundations of Software Engineering, pages 96-106, 2015.
G. Sibay, S. Uchitel, and V. Braberman. Existential live sequence charts revisited. In Proceedings of
the 30th international conference on Software engineering, pages 41-50, 2008.
Downloads
Published
Issue
Section
License
Copyright (c) 2021 Fernando Asteasuain, Federido Calonge, Manuel Dubinsky, Pablo Gamboa
This work is licensed under a Creative Commons Attribution 4.0 International License.
CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).
