Synthesizing partial component-level behavior models from system specifications
Abstract
Initial system specifications, such as use-case scenarios and properties, only partially specify the future system. We posit that synthesizing partial component-level behavior models from these early specifications can improve software development practices. In this paper, we provide a novel algorithm for deriving a Modal Transition System (MTS) for individual system components from system-level scenario and property specifications. The generated MTSs capture the possible component implementations that (1) necessarily provide the behavior required by the scenarios, (2) restrict behavior forbidden by the properties, and (3) leave the behavior that is neither explicitly required nor forbidden as undefined. We also show how our algorithm helps to discover potential design flaws.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Operational profiles can significantly improve the effectiveness of testing by more accurately representing real-world system use.
“operational profiles can significantly improve the effectiveness of testing by more accurately representing real-world system use [7, 50]”
From Fairness testing: testing software for discrimination (2017) · cites this paper as [50]
The citation lists haven’t been fetched yet
References 27 · Cited by 40
- Authors
- Krka, I., Brun, Y., Edwards, G., & Medvidovic, N.
- Affiliations
- University of Southern California (US)
- University of Southern California, Los Angeles, CA, USA
- ORCID
- Brun, Yuriy
- Venue
- Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering
- Publisher
- ACM
- Published
- 2009-08-24
- Pages
- 305-314
- OpenAlex
- W2123042765
- Cited by
- 40
- References
- 27
- Citations by year
- 2021: 1 · 2020: 1 · 2019: 2 · 2018: 2 · 2017: 1 · 2016: 1 · 2015: 3 · 2014: 6 · 2013: 3 · 2012: 9
- FWCI
- 5.76
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) (publishedVersion)
- Funders
- National Science Foundation
- Topics
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
- Physical Sciences › Computer Science › Software › Model-Driven Software Engineering Techniques
- Physical Sciences › Computer Science › Artificial Intelligence › Advanced Software Engineering Methodologies
- Keywords
- modal transition systems, use case scenarios, system characteristics, partial specifications, design flaw detection, software development practices, model-based design
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
