Proving feature non-interaction with Alternating-Time Temporal Logic

Franck Cassez, Mark Ryan, Pierre-Yves Schobbens

Research output: Contribution in Book/Catalog/Report/Conference proceedingConference contribution

Abstract

When engineers design a system with features, they wish to have methods to prove that the features do not interact in ways which are undesirable. One approach to demonstrating that features do not interact undesirably is to equip them with properties which are intended to hold of a system having the feature. In this view, a feature is a pair consisting of the implementation of the feature and a set of properties. Integrating a feature with a base system consists of modifying the base system in the way described by the feature implementation. The integration is deemed successful if the resulting system satisfies the properties of the feature (and of the base system). Evidence that a feature does not negatively interact with second feature may be obtained by verifying that introducing the second feature does not destroy the properties of the first feature.
Original languageEnglish
Title of host publicationLanguage Constructs for Describing Features
Subtitle of host publicationProceedings of the FIREworks workshop
EditorsS Gilmore, M. D Ryan
Place of PublicationLondon
PublisherSpringer
Pages85-103
Number of pages19
Publication statusPublished - 2000

Keywords

  • features integration
  • features interaction
  • simulation
  • features
  • alternating-time temporal logic
  • ATL

Fingerprint

Dive into the research topics of 'Proving feature non-interaction with Alternating-Time Temporal Logic'. Together they form a unique fingerprint.

Cite this