Composing Modal Properties of Programs with Procedures

Marieke Huisman, Dilian Gurov

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

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.
Original languageEnglish
Title of host publicationProceedings of the Formal Foundations of Embedded Software and Component-Based Software Architectures (FESCA 2007)
Subtitle of host publication24 March 2007 • Braga, Portugal
EditorsJ.K.F. Bowles, I. Poernomo, R. Reussner
PublisherElsevier
Pages87-101
Number of pages15
DOIs
Publication statusPublished - 2009
Externally publishedYes
EventFormal Foundations of Embedded Software and Component-Based Software Architectures, FESCA 2007 - Braga, Portugal
Duration: 24 Mar 200724 Mar 2007

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Number7
Volume203
ISSN (Print)1571-0661

Conference

ConferenceFormal Foundations of Embedded Software and Component-Based Software Architectures, FESCA 2007
Abbreviated titleFESCA
CountryPortugal
CityBraga
Period24/03/0724/03/07

Fingerprint Dive into the research topics of 'Composing Modal Properties of Programs with Procedures'. Together they form a unique fingerprint.

Cite this