Specification patterns can be formal and still easy
Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satis...
Guardado en:
| Autor principal: | |
|---|---|
| Publicado: |
2010
|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18917062_v_n_p430_Asteasuain http://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain |
| Aporte de: |
| Sumario: | Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satisfied. When validating the pattern the developer may have to deal with the pattern expressed in some particular formalism. For this reason, we identify three desirable quality attributes for the underlying specification language: succinctness, ease of validation and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. In this work we propose FVS, a graphical scenario-based language, as a possible alternative to specify behavioral properties. We illustrate FVS' features by describing one of the most commonly used pattern, the Response Pattern, and several variants of it. Other known patterns such as the Precedence pattern and the Constrained Chain pattern are also discussed. We also thoroughly compare FVS against other used approaches. |
|---|