Abstract | ||
---|---|---|
Event-B is a formal method for reliable systems specification and verification, which uses model refinement and decomposition as techniques to scale the design of complex systems. In previous work, we proposed an iterative approach for test generation and state model inference based on a variant of Angluin's learning algorithm, which integrates well with the notion of Event-B refinement. In this paper, we extend the method to work also with the mechanisms of Event-B decomposition. Two types of decomposition, i.e. shared-events and shared-variables, are considered and the generation of a global test suite from the local ones is proposed at the end. The implementation of the method is evaluated on publicly available Event-B decomposed models. |
Year | DOI | Venue |
---|---|---|
2012 | 10.1007/978-3-642-34026-0_40 | ISoLA (1) |
Keywords | Field | DocType |
formal method,event-b refinement,event-b decomposition,reliable systems specification,global test suite,state model inference,test generation,available event-b decomposed model,previous work,model refinement | Complex system,Test suite,Inference,Computer science,Algorithm,Theoretical computer science,Regular language,Formal methods,Global variable,Decomposition,Model learning | Conference |
Citations | PageRank | References |
3 | 0.42 | 25 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Ionut Dinca | 1 | 10 | 1.88 |
Florentin Ipate | 2 | 419 | 43.20 |
Alin Stefanescu | 3 | 209 | 17.79 |