Taming interface specifications

Tiziana Margaria, A. Prasad Sistla, Bernhard Steffen, Lenore D. Zuck

Research output: Contribution to journalConference articlepeer-review

Abstract

Software is often being assembled using third-party components where the developers have little knowledge of, and even less control over, the internals of the components comprising the overall system. One obstacle to composing agents is that current formal methods are mainly concerned with "closed" systems that are built from the ground up. Such systems are fully under the control of the user. Hence, problems arising from ill-specified components can be resolved by a close inspection of the systems. When composing systems using "off-the-shelf" components, this is often no longer the case. The paper addresses the problem of under-specification, where an off-the-shelf component does only what it claims to do, however, it claims more behaviors than it actually has and that one wishes for, some of which may render it useless. Given such an under-specified module, we propose a method to automatically synthesize some safety properties from it that would tame its "bad" behaviors. The advantage of restricting to safety properties is that they are monitorable. The safety properties are derived using an automata-theoretic approach. We show that, when restricting to ω-regular languages, there is no maximal safety property. For this case we construct a sequence of increasingly larger safety properties. We also show how to construct an infinite-state automata that can capture any safety property that is contained in the original specifications.

Original languageEnglish
Pages (from-to)548-561
Number of pages14
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3653
DOIs
Publication statusPublished - 2005
Externally publishedYes
Event16th International Conference on Concurrency Theory, CONCUR 2005 - San Francisco, CA, United States
Duration: 23 Aug 200526 Aug 2005

Fingerprint

Dive into the research topics of 'Taming interface specifications'. Together they form a unique fingerprint.

Cite this