A Method for Model Checking Feature Interactions
| Autor: | Arne Skou, Thomas Pedersen, Anders P. Ravn, Thibaut Le Guilly |
|---|---|
| Přispěvatelé: | Lorenz, Pascal, Maciaszek, Leszek |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
Model checking
Theoretical computer science Model driven development business.industry Computer science Real-time computing Model-driven Development Control Systems Automaton Model Checking Formalism (philosophy of mathematics) Home Automation Home automation Control system Timed Automata business Reactive system Feature Interaction |
| Zdroj: | Pedersen, T, Le Guilly, T, Ravn, A P & Skou, A J 2015, A Method for Model Checking Feature Interactions . in P Lorenz & L Maciaszek (eds), Proceedings of the 10th International Conference on Software Engineering and Applications . SCITEPRESS Digital Library, pp. 219-228, 10th International Conference on Software Engineering and Applications, Colmar, Alsace, France, 22/07/2015 . https://doi.org/10.5220/0005516402190228 ICSOFT-EA |
| DOI: | 10.5220/0005516402190228 |
| Popis: | This paper presents a method to check for feature interactions in a system assembled from independently developed concurrent processes as found in many reactive systems. The method combines and refines existing definitions and adds a set of activities. The activities describe how to populate the definitions with models to ensure that all interactions are captured. The method is illustrated on a home automation example with model checking as analysis tool. In particular, the modelling formalism is timed automata and the analysis uses UPPAAL to find interactions. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|