Proving feature non-interaction with Alternating-Time Temporal Logic

Franck Cassez, Mark Ryan, Pierre-Yves Schobbens

Résultats de recherche: Contribution dans un livre/un catalogue/un rapport/dans les actes d'une conférenceArticle dans les actes d'une conférence/un colloque

Résumé

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.
langue originaleAnglais
titreLanguage Constructs for Describing Features
Sous-titreProceedings of the FIREworks workshop
rédacteurs en chefS Gilmore, M. D Ryan
Lieu de publicationLondon
EditeurSpringer
Pages85-103
Nombre de pages19
Etat de la publicationPublié - 2000

Empreinte digitale

Examiner les sujets de recherche de « Proving feature non-interaction with Alternating-Time Temporal Logic ». Ensemble, ils forment une empreinte digitale unique.

Contient cette citation