More Web Proxy on the site http://driver.im/

research-article

Open access

Validating the correctness of reactive systems specifications through systematic exploration

Authors:

Roey RoziAuthors Info & Claims

MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems

Pages 132 - 142

https://doi.org/10.1145/3550355.3552425

Published: 24 October 2022 Publication History

Abstract

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may be incorrect w.r.t. the engineers' intention or w.r.t. the requirements or the environment in which the system should execute in. It thus requires validation.

Combinatorial coverage (CC) is a well-known coverage criterion. Its rationale and key for effectiveness is the empirical observation that in many cases, the presence of a defect depends on the interaction between a small number of features of the system at hand.

In this work we propose a validation approach for a reactive system specification, based on a systematic combinatorial exploration of the behaviors of a controller that was synthesized from it. Specifically, we present an algorithm to generate and execute a small scenario suite that covers all tuples of given variable value combinations over the reachable states of the controller.

We have implemented our work in the Spectra synthesis environment. We evaluated it over benchmarks from the literature using a mutation approach, specifically tailored for evaluating scenario suites of temporal specifications for reactive synthesis. The evaluation shows that for pairwise coverage, our CC algorithms are feasible and provide a 1.7 factor of improvement in mutation score compared to random scenario generation. We further report on a user study with students who have participated in a workshop class at our university and have used our tool to validate their specifications. The user study results demonstrate the potential effectiveness of our work in helping engineers detect real bugs in the specifications they write.

References

[1]

[n.d.]. Spectra Website. http://smlab.cs.tau.ac.il/syntech/spectra/.

[2]

[n.d.]. Supporting Materials Website. https://smlab.cs.tau.ac.il/syntech/validate/.

[3]

David Adamo, Dmitry Nurmuradov, Shraddha Piparia, and Renée C. Bryce. 2018. Combinatorial-based event sequence testing of Android applications. Inf. Softw. Technol. 99 (2018), 98--117.

Digital Library

[4]

Gal Amram, Shahar Maoz, Itai Segall, and Matan Yossef. 2022. Dynamic Update for Synthesized GR(1) Controllers. In ICSE. ACM, 786--797.

Digital Library

[5]

J. H. Andrews, L. C. Briand, Y. Labiche, and A. S. Namin. 2006. Using Mutation Analysis for Assessing and Comparing Testing Coverage Criteria. IEEE Trans. on Software Engineering 32, 8 (2006), 608--624.

Digital Library

[6]

K. Z. Bell and M. A. Vouk. 2005. On effectiveness of pairwise methodology for testing network-centric software. In ICICT. IEEE, 221--235.

[7]

Paul E. Black, Vadim Okun, and Yaacov Yesha. 2000. Mutation Operators for Specifications. In ASE. IEEE, 81.

[8]

Roderick Bloem, Alessandro Cimatti, Karin Greimel, Georg Hofferek, Robert Könighofer, Marco Roveri, Viktor Schuppan, and Richard Seeber. 2010. RATSY - A New Requirements Analysis Tool with Synthesis. In CAV (LNCS), Vol. 6174. Springer, 425--429.

Digital Library

[9]

Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Martin Weiglhofer. 2007. Specify, Compile, Run: Hardware from PSL. Electr. Notes Theor. Comput. Sci. 190, 4 (2007), 3--16.

Digital Library

[10]

Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. 2012. Synthesis of Reactive(1) Designs. J. Comput. Syst. Sci. 78, 3 (2012), 911--938.

Digital Library

[11]

Richard E Boyatzis. 1998. Transforming qualitative information: Thematic analysis and code development. SAGE.

[12]

Randal E. Bryant. 1986. Graph-Based Algorithms for Boolean Function Manipulation. IEEE Trans. Computers 35, 8 (1986), 677--691.

Digital Library

[13]

K. Burroughs, A. Jain, and R.L. Erickson. 1994. Improved quality of protocol testing through techniques of experimental design. In SUPERCOMM/ICC. 745--752.

[14]

Davide G. Cavezza and Dalal Alrajeh. 2017. Interpolation-Based GR(1) Assumptions Refinement. In TACAS (LNCS), Vol. 10205. 281--297.

[15]

Davide G. Cavezza, Dalal Alrajeh, and András György. 2019. Minimal Assumptions Refinement for GR(1) Specifications. CoRR abs/1910.05558 (2019). arXiv:1910.05558 http://arxiv.org/abs/1910.05558

[16]

Alessandro Cimatti, Marco Roveri, Viktor Schuppan, and Andrei Tchaltsev. 2008. Diagnostic Information for Realizability. In VMCAI (LNCS), Vol. 4905. Springer, 52--67.

[17]

E. M. Clarke, O. Grumberg, and D. A. Peled. 1999. Model Checking. The MIT Press.

[18]

D. M. Cohen, S. R. Dalal, M. L. Fredman, and G. C. Patton. 1997. The AETG System: An Approach to Testing Based on Combinatorial Design. IEEE Trans. on Softw. Eng. 23, 7 (1997), 437--444.

Digital Library

[19]

Myra B. Cohen, Matthew B. Dwyer, and Jiangfan Shi. 2008. Constructing Interaction Test Suites for Highly-Configurable Systems in the Presence of Constraints: A Greedy Approach. IEEE Trans. Software Eng. 34, 5 (2008), 633--650.

Digital Library

[20]

M. B. Cohen, J. Snyder, and G. Rothermel. 2006. Testing across configurations: implications for combinatorial testing. SIGSOFT Softw. Eng. Notes 31, 6 (2006), 1--9.

Digital Library

[21]

S. R. Dalal, A. Jain, N. Karunanithi, J. M. Leaton, C. M. Lott, G. C. Patton, and B. M. Horowitz. 1999. Model-Based Testing in Practice. In ICSE. 285--294.

[22]

Elizabeth Firman, Shahar Maoz, and Jan Oliver Ringert. 2020. Performance heuristics for GR(1) synthesis and related algorithms. Acta Informatica 57, 1--2 (2020), 37--79.

[23]

Gordon Fraser and Franz Wotawa. 2009. Complementary Criteria for Testing Temporal Logic Properties. In Tests and Proofs, Catherine Dubois (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 58--73.

[24]

M. Grindal, B. Lindström, J. Offutt, and S. F. Andler. 2006. An evaluation of combination strategies for test case selection. Empirical Softw. Eng. 11, 4 (2006), 583--611.

Digital Library

[25]

René Just, Darioush Jalali, Laura Inozemtseva, Michael D. Ernst, Reid Holmes, and Gordon Fraser. 2014. Are mutants a valid substitute for real faults in software testing?. In FSE. ACM, 654--665.

Digital Library

[26]

B.A. Kitchenham, S.L. Pfleeger, L.M. Pickard, P.W. Jones, D.C. Hoaglin, K. El Emam, and J. Rosenberg. 2002. Preliminary guidelines for empirical research in software engineering. IEEE Transactions on Software Engineering 28, 8 (2002), 721--734.

Digital Library

[27]

Robert Könighofer, Georg Hofferek, and Roderick Bloem. 2013. Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. STTT 15, 5--6 (2013), 563--583.

Digital Library

[28]

Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. 2009. Temporal-Logic-Based Reactive Mission and Motion Planning. IEEE Trans. Robotics 25, 6 (2009), 1370--1381.

Digital Library

[29]

D. R. Kuhn, Raghu N. Kacker, and Y. Lei. 2013. Introduction to Combinatorial Testing. Chapman & Hall/CRC.

[30]

D. R. Kuhn and M. J. Reilly. 2002. An Investigation of the Applicability of Design of Experiments to Software Testing. 27th NASA/IEEE Software Engineering Workshop, NASA Goddard Space Flight Center.

[31]

D. R. Kuhn, D. R. Wallace, and A. M. Gallo, Jr. 2004. Software Fault Interactions and Implications for Software Testing. IEEE Trans. Softw. Eng. 30, 6 (2004), 418--421.

Digital Library

[32]

Y. Lei and K.-C. Tai. 1998. In-Parameter-Order: A Test Generation Strategy for Pairwise Testing. In The 3rd IEEE International Symposium on High-Assurance Systems Engineering (HASE '98). 254--261.

[33]

Spyros Maniatopoulos, Philipp Schillinger, Vitchyr Pong, David C. Conner, and Hadas Kress-Gazit. 2016. Reactive high-level behavior synthesis for an Atlas humanoid robot. In ICRA, Danica Kragic, Antonio Bicchi, and Alessandro De Luca (Eds.). IEEE, 4192--4199.

Digital Library

[34]

Shahar Maoz and Jan Oliver Ringert. 2015. GR(1) synthesis for LTL specification patterns. In ESEC/FSE. ACM, 96--106.

Digital Library

[35]

Shahar Maoz and Jan Oliver Ringert. 2021. Spectra: a specification language for reactive systems. Softw. Syst. Model. 20, 5 (2021), 1553--1586.

Digital Library

[36]

Shahar Maoz, Jan Oliver Ringert, and Rafi Shalom. 2019. Symbolic repairs for GR(1) specifications. In ICSE. IEEE / ACM, 1016--1026. https://dl.acm.org/citation.cfm?id=3339632

[37]

Shahar Maoz and Rafi Shalom. 2020. Inherent Vacuity for GR(1) Specifications. In ESEC/FSE. 99--110.

[38]

Shahar Maoz and Rafi Shalom. 2021. Unrealizable Cores for Reactive Systems Specifications. In ICSE. IEEE, 25--36.

Digital Library

[39]

Shahar Maoz and Ilia Shevrin. 2020. Just-In-Time Reactive Synthesis. In ASE. IEEE, 635--646.

Digital Library

[40]

Claudio Menghi, Christos Tsigkanos, Patrizio Pelliccione, Carlo Ghezzi, and Thorsten Berger. 2019. Specification Patterns for Robotic Missions. CoRR abs/1901.02077 (2019). arXiv:1901.02077 http://arxiv.org/abs/1901.02077

[41]

Cu D. Nguyen, Alessandro Marchetto, and Paolo Tonella. 2012. Combining model-based and combinatorial testing for effective test case generation. In ISSTA. ACM, 100--110.

Digital Library

[42]

Justyna Petke, Myra B. Cohen, Mark Harman, and Shin Yoo. 2015. Practical Combinatorial Interaction Testing: Empirical Findings on Efficiency and Early Fault Detection. IEEE Trans. Software Eng. 41, 9 (2015), 901--924.

Digital Library

[43]

Amir Pnueli and Roni Rosner. 1989. On the Synthesis of a Reactive Module. In POPL. ACM Press, 179--190.

[44]

Xiao Qu, Myra B. Cohen, and Katherine M. Woolf. 2007. Combinatorial Interaction Regression Testing: A Study of Test Case Generation and Prioritization. In ICSM. IEEE Computer Society, 255--264.

[45]

I. Segall, R. Tzoref-Brill, and E. Farchi. 2011. Using Binary Decision Diagrams for Combinatorial Test Design. In Proceedings of the 2011 International Symposium on Software Testing and Analysis (ISSTA '11). 254--264.

[46]

Fabio Somenzi. 2015. CUDD: CU Decision Diagram Package Release 3.0.0. http://vlsi.colorado.edu/~fabio/CUDD/cudd.pdf.

[47]

M. Trakhtenbrot. 2017. Mutation Patterns for Temporal Requirements of Reactive Systems. In 2017 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW). 116--121.

[48]

Rachel Tzoref-Brill. 2019. Chapter Two - Advances in Combinatorial Testing. Adv. Comput. 112 (2019), 79--134.

[49]

D. R. Wallace and D. R. Kuhn. 2001. Failure Modes in Medical Device Software: an Analysis of 15 Years of Recall Data. In ACS/IEEE International Conference on Computer Systems and Applications. 301--311.

[50]

Eric Wete, Joel Greenyer, Andreas Wortmann, Oliver Flegel, and Martin Klein. 2021. Monte Carlo Tree Search and GR(1) Synthesis for Robot Tasks Planning in Automotive Production Lines. In MODELS. IEEE, 320--330.

[51]

A. W. Williams. 2000. Determination of Test Configurations for Pair-Wise Interaction Coverage. In TestCom. 59--74.

[52]

P. Wojciak and R. Tzoref-Brill. 2014. System Level Combinatorial Testing in Practice - The Concurrent Maintenance Case Study. In ICST. 103--112.

[53]

Huayao Wu, Changhai Nie, Justyna Petke, Yue Jia, and Mark Harman. 2020. An Empirical Comparison of Combinatorial Testing, Random Testing and Adaptive Random Testing. IEEE Trans. Software Eng. 46, 3 (2020), 302--320.

Digital Library

[54]

Akihisa Yamada, Armin Biere, Cyrille Artho, Takashi Kitamura, and Eun-Hye Choi. 2016. Greedy combinatorial test case generation using unsatisfiable cores. In ASE. ACM, 614--624.

Digital Library

[55]

Z. Zhang and J. Zhang. 2011. Characterizing Failure-causing Parameter Interactions by Adaptive Testing. In ISSTA. 331--341.

Cited By

Martins L(2024)From Textual to Formal Requirements: A Case Study Using Spectra in Safety-Critical Systems DomainJournal of Software Engineering Research and Development10.5753/jserd.2024.374512:1Online publication date: 4-Nov-2024
https://doi.org/10.5753/jserd.2024.3745
Ma'ayan DMaoz SGrundy JPollock LPenta M(2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00071

Recommendations

Validating feature-based specifications: Research Articles

It is argued that specifications should be rigorously validated against requirements. This is useful to build confidence in a specification and to check a specification after it or the requirements have changed. The multiple-use scenario test and ...
System Requirements and Formal Specifications of Hierarchical Reactive Systems
ICPADS '00: Proceedings of the Seventh International Conference on Parallel and Distributed Systems

A methodology for the description of system requirements and formal specifications of reactive systems, and the synthesis of formal specifications is presented. Based on a hierarchical structure of system properties a hierarchical assertional language ...
Finding the Causes of Unrealizability of Reactive System Formal Specifications
SEFM '04: Proceedings of the Software Engineering and Formal Methods, Second International Conference

Reactive systems are the systems that maintain some interaction with their environment. Temporal logic is one of the methods for formal specification descriptions of reactive systems. The formal specifications of reactive systems enables to check the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

MODELS '22: Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems

October 2022

412 pages

ISBN:9781450394666

DOI:10.1145/3550355

General Chairs:
Eugene Syriani
Université de Montréal, Canada
,
Houari Sahraoui
Université de Montréal, Canada

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

Univ. of Montreal: University of Montreal
IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 24 October 2022

Check for updates

Badges

Artifacts Evaluated & Reusable / v1.1

Qualifiers

Research-article

Funding Sources

European Research Council (ERC)

Conference

MODELS '22

Sponsor:

SIGSOFT

MODELS '22: ACM/IEEE 25th International Conference on Model Driven Engineering Languages and Systems

October 23 - 28, 2022

Quebec, Montreal, Canada

Acceptance Rates

MODELS '22 Paper Acceptance Rate 35 of 125 submissions, 28%;

Overall Acceptance Rate 144 of 506 submissions, 28%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
313
Total Downloads

Downloads (Last 12 months)119
Downloads (Last 6 weeks)15

Reflects downloads up to 25 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Martins L(2024)From Textual to Formal Requirements: A Case Study Using Spectra in Safety-Critical Systems DomainJournal of Software Engineering Research and Development10.5753/jserd.2024.374512:1Online publication date: 4-Nov-2024
https://doi.org/10.5753/jserd.2024.3745
Ma'ayan DMaoz SGrundy JPollock LPenta M(2023)Using Reactive Synthesis: An End-to-End Exploratory Case StudyProceedings of the 45th International Conference on Software Engineering10.1109/ICSE48619.2023.00071(742-754)Online publication date: 14-May-2023
https://dl.acm.org/doi/10.1109/ICSE48619.2023.00071

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten