Back to Search
Start Over
Domain-Specific Scenarios for Refinement-Based Methods
- Source :
- Communications in Computer and Information Science ISBN: 9783030322120, MEDI Workshops
- Publication Year :
- 2019
- Publisher :
- Springer International Publishing, 2019.
-
Abstract
- Formal methods use abstraction and rigorously verified refinement to manage the design of complex systems, ensuring that they satisfy important invariant properties. However, formal verification is not sufficient: models must also be tested to ensure that they behave according to the informal requirements and validated by domain experts who may not be expert in formal modelling. This can be satisfied by scenarios that complement the requirements specification. The model can be animated to check that the scenario is feasible in the model and that the model reaches states expected in the scenario. However, there are two problems with this approach. (1) The provided scenarios are at the most concrete level corresponding to the full requirements and cannot be used until all the refinements have been completed in the model. (2) The natural language used to describe the scenarios is often verbose, ambiguous and therefore difficult to understand; especially if the modeller is not a domain expert. In this paper we propose a method of abstracting scenarios from concrete ones so that they can be used to test early refinements of the model. We also show by example how a precise and concise domain specific language can be used for writing these abstract scenarios in a style that can be easily understood by the domain expert (for validation purposes) as well as the modeller (for behavioural verification). We base our approach on the Cucumber framework for scenarios and the Event-B modelling language and tool set. We illustrate the proposed methods on the ERTMS/ETCS Hybrid Level 3 specification for railway controls (The example model and scenario scripts supporting this paper are openly available at https://doi.org/10.5258/SOTON/D1026).
- Subjects :
- 010302 applied physics
Domain-specific language
business.industry
Computer science
Complex system
Software requirements specification
02 engineering and technology
computer.software_genre
Formal methods
01 natural sciences
Subject-matter expert
Scripting language
0103 physical sciences
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Software engineering
business
computer
Formal verification
Natural language
Subjects
Details
- ISBN :
- 978-3-030-32212-0
- ISBNs :
- 9783030322120
- Database :
- OpenAIRE
- Journal :
- Communications in Computer and Information Science ISBN: 9783030322120, MEDI Workshops
- Accession number :
- edsair.doi.dedup.....53677fc3452ffc4b36ccb3d91712c8e7
- Full Text :
- https://doi.org/10.1007/978-3-030-32213-7_2