Loading...
Please wait, while we are loading the content...
Proving feature non-interaction with alternating-time temporal logic
| Content Provider | Semantic Scholar |
|---|---|
| Author | Cassez, Franck Ryan, Mark Schobbens, Pierre-Yves |
| Copyright Year | 2001 |
| Abstract | Feature Interaction. 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. A considerable literature is devoted to this ‘feature interaction problem’ [13,5]. 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 [18]. In this view, a feature is a pair (F, o) consisting of the implementation of the feature F and a set of properties o. Integrating a feature (F, o) with a base system S consists of modifying the base system in the way described by the feature implementation and obtaining S + F. The integration is deemed successful if the resulting system satisfies the set of properties o corresponding to the feature. Evidence that a feature (F 1, o1) does not negatively interact with feature (F 2, o2) may be obtained by verifying that introducing F 2 in S + F 1 , (obtaining S + F 1 + F 2) does not destroy the properties o1 previous introduced by feature F 1, and vice versa. |
| Starting Page | 85 |
| Ending Page | 103 |
| Page Count | 19 |
| File Format | PDF HTM / HTML |
| DOI | 10.1007/978-1-4471-0287-8_6 |
| Alternate Webpage(s) | http://www.cs.bham.ac.uk/~mdr/research/papers/pdf/00-atl.pdf |
| Alternate Webpage(s) | https://www.cs.bham.ac.uk/~mdr/research/papers/pdf/00-atl.pdf |
| Alternate Webpage(s) | http://www.dcs.ed.ac.uk/~stg/fireworks/book/Cassez/atl6.ps |
| Alternate Webpage(s) | http://www.dcs.ed.ac.uk/home/stg/fireworks/book/Cassez/atl6.ps |
| Alternate Webpage(s) | https://doi.org/10.1007/978-1-4471-0287-8_6 |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
