Abstract | ||
---|---|---|
To analyse the behaviour of reactive systems formally, it is necessary to build a model. At the very beginning of the development, typically only natural language requirements are documented. We present a formal model, named Data-Flow Reactive Systems (DFRS), which can be automatically obtained from natural language requirements that may also describe temporal properties. We prove that a DFRS can be mapped to a timed input-output transition system, which is widely used to characterise conformance relations for timed reactive systems. To validate the proposed model as well as the mechanisation developed to support its analysis, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-319-11737-9_4 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
Model mapping,TIOTS,test-case generation | Aerospace,Transition system,Software engineering,Computer science,Theoretical computer science,Natural language,Test case,Reactive system,Natural language requirements,Automotive industry | Conference |
Volume | ISSN | Citations |
8829 | 0302-9743 | 2 |
PageRank | References | Authors |
0.39 | 16 | 5 |
Name | Order | Citations | PageRank |
---|---|---|---|
Gustavo Carvalho | 1 | 48 | 6.13 |
Ana Carvalho | 2 | 9 | 0.98 |
Eduardo Rocha | 3 | 2 | 0.39 |
Ana Cavalcanti | 4 | 668 | 59.95 |
Augusto Sampaio | 5 | 501 | 43.38 |