J.C. Campos and J. Machado
Supporting requirements formulation in software formal verification
In Ambrosio, A.M., Mattiello-Francisco, M.F., Batista, J.C., Barbosa, R. and Cancela, H., editors, Latin-American Symposium on Dependable Computing (LADC 2011) suplemental proceedings. INPE. 2011.

Abstract

Formal verification tools such as model checkers have reached a stage were their applicability in the development process of dependable and safety critical systems has become viable. While the formal verification step in tools such as model checkers is fully automated, writing appropriate models and properties is a skillful process. In particular, a correct understanding of the logics used to express properties is needed to guarantee that properties correctly encode the original requirements. In this paper we illustrate how a patterns-based tool can help in simplifying the process of generating logical formulae from informally expressed requirements.

download PDF

@InProceedings{CamposM:2011,
 author = {J.C. Campos and J. Machado},
 title = {Supporting requirements formulation in software formal verification},
 booktitle = {Latin-American Symposium on Dependable Computing (LADC 2011) suplemental proceedings},
 abstract = {Formal verification tools such as model checkers have reached a stage were their applicability in the development process of dependable and safety critical systems has become viable. While the formal verification step in tools such as model checkers is fully automated, writing appropriate models and properties is a skillful process. In particular, a correct understanding of the logics used to express properties is needed to guarantee that properties correctly encode the original requirements. In this paper we illustrate how a patterns-based tool can help in simplifying the process of generating logical formulae from informally expressed requirements.},
 editor = {Ambrosio, A.M. and Mattiello-Francisco, M.F. and Batista, J.C. and Barbosa, R. and Cancela, H.},
 paperurl = {http://mtc-m18.sid.inpe.br/rep/sid.inpe.br/mtc-m18/2011/04.11.16.56?mirror=sid.inpe.br/mtc-m18@80/2008/03.17.15.17.24&metadatarepository=sid.inpe.br/mtc-m18/2011/04.11.16.56.36},
 year = {2011},
 publisher = {INPE}
}

Generated by mkBiblio 2.6.23