Verificación de propiedades de escenarios utilizando puntos fijos (Verifying Properties of Scenarios with Fixed Points)

Ricardo Wehbe (rwehbe@uade.edu.ar)


Universidad Argentina de la Empresa
This paper appears in: Revista IEEE América Latina

Publication Date: Feb. 2013
Volume: 11,   Issue: 1 
ISSN: 1548-0992


Abstract:
During the requirements elicitation phase a software engineer tries to determine what the customer really wants (and needs.) This task requires, on the one hand, strong communication skills and, on the other hand, a good engineering background to construct a coherent set of requirements. There is a thus a conflict informal and formal techniques. Scenarios are a powerful communication tool and may be given a formal semantics so that they may be amenable to formal verification. We present a method to verifying properties of scenarios based on fixed points of predicate transformers. This work is adapted from an approach that had been originally proposed by Sifakis for transition systems. Scenarios are modelled in a similar way to Diijkstras guarded commands.

Index Terms:
Software Engineering, Formal Verification.   


Documents that cite this document
This function is not implemented yet.


[PDF Full-Text (230)]