Changeset 89 for papers/FDL2012/FDL2012.tex
- Timestamp:
- Apr 6, 2012, 4:44:06 PM (12 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/FDL2012.tex
r83 r89 85 85 %\section*{Drawbacks} 86 86 87 We have presented a new strategy in the abstraction generation and refinement which is well adapted for compositional embedded systems. This verification technique is compatible and suits well in the natural development process of complex systems. Our preliminary experimental results shows an interesting performance in terms duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph. 87 We have presented a new strategy in the abstraction generation and refinement 88 which is well adapted for compositional embedded systems. This verification 89 technique is compatible and suits well in the natural development process of 90 complex systems. Our preliminary experimental results shows an interesting 91 performance in terms of duration of abstraction generation and the number of refinement iteration. Futhermore, this technique enables us to overcome repetitive counterexamples due to the presence of cycles in the system's graph. 88 92 89 Nevertheless, in order to function well, this refinement technique requires a complete specification of every components of the concrete model. Futhermore, it may be possible that none of the properties available is capable of eliminating the counterexample which probably due to the fact that the specification is not complete or counterexample given is provoqued by the composition of components. In this case, other refinement techniques such as the refinement by eliminating the counterexample only techniques should be considered. We are currently investigating other complementary techniques to overcome these particular cases. 93 Nevertheless, in order to function well, this refinement technique requires a 94 complete specification of every components of the concrete model. Futhermore, 95 it may be possible that none of the properties available is capable of 96 eliminating the counterexample which is probably due to an uncomplete 97 specification or a counterexample that should be eliminated by the product of 98 local properties. In this case, other refinement techniques such as the 99 refinement by eliminating the counterexample only, or the identification of a 100 good set of local properties to be integreted simultaneously, should be considered. 101 We are currently investigating other complementary techniques to overcome these particular cases. 102 A complementary approach consists in oimproving the specification of the 103 model~: at the component level, or for groups of components. The work of 104 Kroening \cite{pwk2009-date} could help us in this direction. 90 105 91 106
Note: See TracChangeset
for help on using the changeset viewer.