TY - GEN
T1 - Composing Modal Properties of Programs with Procedures
AU - Huisman, Marieke
AU - Gurov, Dilian
PY - 2009
Y1 - 2009
N2 - In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion.
AB - In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion.
U2 - 10.1016/j.entcs.2009.03.028
DO - 10.1016/j.entcs.2009.03.028
M3 - Conference contribution
T3 - Electronic Notes in Theoretical Computer Science
SP - 87
EP - 101
BT - Proceedings of the Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007)
A2 - Bowles, J.K.F.
A2 - Poernomo, I.
A2 - Reussner, R.
PB - Elsevier
T2 - Formal Foundations of Embedded Software and Component-Based Software Architectures, FESCA 2007
Y2 - 24 March 2007 through 24 March 2007
ER -