Abstract | ||
---|---|---|
A framework based on the notion of conflict-tolerance was proposed in [1] as a methodology for developing and reasoning about systems that are composed of multiple independent features. In [1], the authors use annotated transition systems to specify conflict-tolerant features. In this paper we propose a way of specifying conflict-tolerant features in temporal logic which is a specification language used in practice. We also provide a method for verifying whether a given feature implementation meets a given feature specification in our logic. The paper concludes by providing a constructive procedure for synthesising a finite-state feature implementation from feature specification in our logic. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1145/1730874.1730894 | ISEC |
Keywords | Field | DocType |
conflict-tolerant specification,feature implementation,temporal logic,finite-state feature implementation,constructive procedure,specification language,feature specification,multiple independent feature,annotated transition system,conflict-tolerant feature | Temporal logic of actions,Horn clause,Interval temporal logic,Computer science,Multimodal logic,Description logic,Linear temporal logic,Theoretical computer science,Language Of Temporal Ordering Specification,Temporal logic | Conference |
Citations | PageRank | References |
2 | 0.42 | 4 |
Authors | ||
3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Sumesh Divakaran | 1 | 3 | 0.80 |
Deepak D'souza | 2 | 239 | 17.90 |
M. Raj Mohan | 3 | 4 | 1.49 |