Publications
2023
- ICSEUsing Reactive Synthesis: An End-to-End Exploratory Case StudyDor Ma’ayan, and Shahar MaozIn IEEE/ACM 45th International Conference on Software Engineering (ICSE), 2023
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Despite its attractiveness and major research progress in the past decades, reactive synthesis is still in early-stage and has not gained popularity outside academia. We conducted an exploratory case study in which we followed students in a semester-long university workshop class on their end-to-end use of a reactive synthesizer, from writing the specifications to executing the synthesized controllers. The data we collected includes more than 500 versions of more than 80 specifications, as well as more than 2500 Slack messages, all written by the class participants. Our grounded theory analysis reveals that the use of reactive synthesis has clear benefits for certain tasks and that adequate specification language constructs assist in the specification writing process. However, inherent issues such as unrealizabilty, non-well-separation, the gap of knowledge between the users and the synthesizer, and considerable running times prevent reactive synthesis from fulfilling its promise. Based on our analysis, we propose action items in the directions of language and specification quality, tools for analysis and execution, and process and methodology, all towards making reactive synthesis more applicable for software engineers.
@inproceedings{Exploratory, author = {Ma'ayan, Dor and Maoz, Shahar}, booktitle = {IEEE/ACM 45th International Conference on Software Engineering (ICSE)}, title = {Using Reactive Synthesis: An End-to-End Exploratory Case Study}, year = {2023}, volume = {}, number = {}, } - ICSETriggers for Reactive Synthesis SpecificationsGal Amram, Dor Ma’ayan, Shahar Maoz, Or Pistiner, and Jan Oliver RingertIn IEEE/ACM 45th International Conference on Software Engineering (ICSE), 2023
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Two of the main challenges in bringing reactive synthesis to practice are its very high worst-case complexity and the difficulty of writing declarative specifications using basic LTL operators. To address the first challenge, researchers have suggested the GR(1) fragment of LTL, which has an efficient polynomial time symbolic synthesis algorithm. To address the second challenge, specification languages include higher-level constructs that aim at allowing engineers to write succinct and readable specifications. One such construct is the triggers operator, as supported, e.g., in the Property Specification Language (PSL). In this work we introduce triggers into specifications for reactive synthesis. The effectiveness of our contribution relies on a novel encoding of regular expressions using symbolic finite automata (SFA) and on a novel semantics for triggers that, in contrast to PSL triggers, admits an efficient translation into GR(1). We show that our triggers are expressive and succinct, and prove that our encoding is optimal. We have implemented our ideas on top of the Spectra language and synthesizer. We demonstrate the usefulness and effectiveness of using triggers in specifications for synthesis, as well as the challenges involved in using them, via a study of more than 300 triggers written by undergraduate students who participated in a project class on writing specifications for synthesis. To the best of our knowledge, our work is the first to introduce triggers into specifications for reactive synthesis.
@inproceedings{Triggers, author = {Amram, Gal and Ma'ayan, Dor and Maoz, Shahar and Pistiner, Or and Ringert, Jan Oliver}, booktitle = {IEEE/ACM 45th International Conference on Software Engineering (ICSE)}, title = {Triggers for Reactive Synthesis Specifications}, year = {2023}, volume = {}, number = {}, } - ICSE NIERAnti-Patterns (Smells) in Temporal SpecificationsDor Ma’ayan, Shahar Maoz, and Jan Oliver RingertIn IEEE/ACM 45th International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), 2023
Temporal specifications are essential inputs for verification and synthesis. Despite their importance, temporal specifications are challenging to write, which might limit their use by software engineers. To this day, almost no quality attributes of temporal specifications have been defined and investigated. Our work takes a first step toward exploring and improving the quality of temporal specifications by proposing a preliminary catalog of anti-patterns (a.k.a. smells). We base the catalog on our experience in developing and teaching temporal specifications for verification and synthesis. In addition, we examined publicly available specification repositories and relevant literature. Finally, we outline our future plans for a better understanding of what constitutes high-quality temporal specifications and the development of tools that will help engineers write them.
@inproceedings{Patterns, author = {Ma'ayan, Dor and Maoz, Shahar and Ringert, Jan Oliver}, booktitle = {IEEE/ACM 45th International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER)}, title = {Anti-Patterns (Smells) in Temporal Specifications}, year = {2023}, volume = {}, number = {}, }
2022
- MODELSValidating the correctness of reactive systems specifications through systematic explorationDor Ma’ayan, Shahar Maoz, and Roey RoziIn Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, MODELS 2022, Montreal, Quebec, Canada, October 23-28, 2022, 2022
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.
@inproceedings{DBLP:conf/models/MaayanMR22, author = {Ma'ayan, Dor and Maoz, Shahar and Rozi, Roey}, editor = {Syriani, Eugene and Sahraoui, Houari A. and Bencomo, Nelly and Wimmer, Manuel}, title = {Validating the correctness of reactive systems specifications through systematic exploration}, booktitle = {Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems, {MODELS} 2022, Montreal, Quebec, Canada, October 23-28, 2022}, pages = {132--142}, publisher = {{ACM}}, year = {2022}, url = {https://doi.org/10.1145/3550355.3552425}, doi = {10.1145/3550355.3552425}, timestamp = {Wed, 07 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/models/MaayanMR22.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }
2020
- SIGGRAPHPenrose: from mathematical notation to beautiful diagramsKatherine Ye, Wode Ni, Max Krieger, Dor Ma’ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, and Keenan CraneACM Transaction on Graphics (SIGGRAPH), 2020
We introduce a system called Penrose for creating mathematical diagrams. Its basic functionality is to translate abstract statements written in familiar math-like notation into one or more possible visual representations. Rather than rely on a fixed library of visualization tools, the visual representation is user-defined in a constraint-based specification language; diagrams are then generated automatically via constrained numerical optimization. The system is user-extensible to many domains of mathematics, and is fast enough for iterative design exploration. In contrast to tools that specify diagrams via direct manipulation or low-level graphics programming, Penrose enables rapid creation and exploration of diagrams that faithfully preserve the underlying mathematical meaning. We demonstrate the effectiveness and generality of the system by showing how it can be used to illustrate a diverse set of concepts from mathematics and computer graphics.
@article{DBLP:journals/tog/YeNKMWASC20, author = {Ye, Katherine and Ni, Wode and Krieger, Max and Ma'ayan, Dor and Wise, Jenna and Aldrich, Jonathan and Sunshine, Joshua and Crane, Keenan}, title = {Penrose: from mathematical notation to beautiful diagrams}, journal = {{ACM Transaction on Graphics (SIGGRAPH)}}, volume = {39}, number = {4}, pages = {144}, year = {2020}, url = {https://doi.org/10.1145/3386569.3392375}, doi = {10.1145/3386569.3392375}, timestamp = {Wed, 07 Dec 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/tog/YeNKMWASC20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, } - CHIHow Domain Experts Create Conceptual Diagrams and Implications for Tool DesignDor Ma’ayan, Wode Ni, Katherine Ye, Chinmay Kulkarni, and Joshua SunshineIn CHI ’20: CHI Conference on Human Factors in Computing Systems, Honolulu, HI, USA, April 25-30, 2020, 2020
Conceptual diagrams are used extensively to understand abstract relationships, explain complex ideas, and solve difficult problems. To illustrate concepts effectively, experts find appropriate visual representations and translate concepts into concrete shapes. This translation step is not supported explicitly by current diagramming tools. This paper investigates how domain experts create conceptual diagrams via semi-structured interviews with 18 participants from diverse backgrounds. Our participants create, adapt, and reuse visual representations using both sketches and digital tools. However, they had trouble using current diagramming tools to transition from sketches and reuse components from earlier diagrams. Our participants also expressed frustration with the slow feedback cycles and barriers to automation of their tools. Based on these results, we suggest four opportunities of diagramming tools — exploration support, representation salience, live engagement, and vocabulary correspondence — that together enable a natural diagramming experience. Finally, we discuss possibilities to leverage recent research advances to develop natural diagramming tools.
@inproceedings{DBLP:conf/chi/MaayanNYKS20, author = {Ma'ayan, Dor and Ni, Wode and Ye, Katherine and Kulkarni, Chinmay and Sunshine, Joshua}, editor = {Bernhaupt, Regina and Mueller, Florian 'Floyd' and Verweij, David and Andres, Josh and McGrenere, Joanna and Cockburn, Andy and Avellino, Ignacio and Goguey, Alix and Bj{\o}n, Pernille and Zhao, Shengdong and Samson, Briane Paul and Kocielnik, Rafal}, title = {How Domain Experts Create Conceptual Diagrams and Implications for Tool Design}, booktitle = {{CHI} '20: {CHI} Conference on Human Factors in Computing Systems, Honolulu, HI, USA, April 25-30, 2020}, pages = {1--14}, publisher = {{ACM}}, year = {2020}, url = {https://doi.org/10.1145/3313831.3376253}, doi = {10.1145/3313831.3376253}, timestamp = {Thu, 23 Jun 2022 19:55:35 +0200}, biburl = {https://dblp.org/rec/conf/chi/MaayanNYKS20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }
2018
- SQUADEThe quality of junit tests: an empirical study reportDor D. Ma’ayanIn Proceedings of the 1st International Workshop on Software Qualities and Their Dependencies, SQUADE@ICSE 2018, Gothenburg, Sweden, May 28, 2018, 2018
The quality of unit tests gains substantial importance in modern software systems. This work explores the way in which Junit tests are written in real world Java systems. We analyse 112 Java repositories and measure the quality of unit tests by finding patterns which indicate good practices of coding. Our results show that the quality of real world unit tests is low, and that in many cases, unit tests don’t follow the well-known recommendations for writing unit tests. These early results demonstrate the need for more tools and techniques for refactoring of tests.
@inproceedings{DBLP:conf/icse/Maayan18, author = {Ma'ayan, Dor D.}, editor = {Sentilles, S{\'{e}}verine and Boehm, Barry W. and Trubiani, Catia and Franch, Xavier and Koziolek, Anne}, title = {The quality of junit tests: an empirical study report}, booktitle = {Proceedings of the 1st International Workshop on Software Qualities and Their Dependencies, SQUADE@ICSE 2018, Gothenburg, Sweden, May 28, 2018}, pages = {33--36}, publisher = {{ACM}}, year = {2018}, url = {https://doi.org/10.1145/3194095.3194102}, doi = {10.1145/3194095.3194102}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/icse/Maayan18.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }
2017
- VISSOFTSyntactic Zoom-Out / Zoom-In Code with the AthenizerYossi Gil, Dor Ma’ayan, Niv Shalmon, Raviv Rachmiel, and Ori RothIn IEEE Working Conference on Software Visualization, VISSOFT 2017, Shanghai, China, September 18-19, 2017, 2017
Care and great e.ort are often taken to dress program code of libraries, just as model implementations, in its most presentable form, which includes adherence to strict coding standards, careful selection of identifiers, avoiding unnecessary constructs, etc. However, a presentable dress is not a janitor’s uniform and is often inferior to the more lax working outfit.The spartanizer is a tool that brings Java code into a canonical, short form. Trying to say the most with the fewest words. In contrast, the athenizer is a tool that expands the code, placing it in a more maintainable form, using plenty of auxiliary variables, many potential locations for breakpoints and for change.The tool reported on here allows developers to interactively use their joystick and its buttons for code navigation, and in particular for zooming-in into the code (athenizing) and zooming-out of it (spartanizing).
@inproceedings{DBLP:conf/vissoft/GilMSRR17, author = {Gil, Yossi and Ma'ayan, Dor and Shalmon, Niv and Rachmiel, Raviv and Roth, Ori}, title = {Syntactic Zoom-Out / Zoom-In Code with the Athenizer}, booktitle = {{IEEE} Working Conference on Software Visualization, {VISSOFT} 2017, Shanghai, China, September 18-19, 2017}, pages = {124--128}, publisher = {{IEEE}}, year = {2017}, url = {https://doi.org/10.1109/VISSOFT.2017.26}, doi = {10.1109/VISSOFT.2017.26}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/vissoft/GilMSRR17.bib}, bibsource = {dblp computer science bibliography, https://dblp.org}, }