Information-flow interfaces

Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. 2024. Information-flow interfaces. Formal Methods in System Design.

Download (ext.)

Journal Article | Epub ahead of print | English

Scopus indexed

Corresponding author has ISTA affiliation

Abstract
Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory designed to ensure system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. Additionally, we introduce information-flow contracts where assumptions and guarantees are sets of flow relations. We use these contracts to illustrate how to enrich information-flow interfaces with a semantic view. We illustrate the applicability of our framework with two examples inspired by the automotive domain.
Publishing Year
Date Published
2024-05-23
Journal Title
Formal Methods in System Design
Publisher
Springer Nature
Acknowledgement
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and it was funded in part by the Austrian Science Fund (FWF) project W1255-N23, by the Austrian FWF project ZK-35, by the FWF project SpyCoDe 10.55776/F85 and by the ERC-2020-AdG 101020093. This paper extends the text and the results of the manuscript published at FASE 2022 [1].
ISSN
eISSN
IST-REx-ID

Cite this

Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-flow interfaces. Formal Methods in System Design. 2024. doi:10.1007/s10703-024-00447-0
Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., & Oliveira da Costa, A. (2024). Information-flow interfaces. Formal Methods in System Design. Springer Nature. https://doi.org/10.1007/s10703-024-00447-0
Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces.” Formal Methods in System Design. Springer Nature, 2024. https://doi.org/10.1007/s10703-024-00447-0.
E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-flow interfaces,” Formal Methods in System Design. Springer Nature, 2024.
Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. 2024. Information-flow interfaces. Formal Methods in System Design.
Bartocci, Ezio, et al. “Information-Flow Interfaces.” Formal Methods in System Design, Springer Nature, 2024, doi:10.1007/s10703-024-00447-0.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]

Link(s) to Main File(s)
Access Level
OA Open Access
Material in ISTA:
Shorter Version

Export

Marked Publications

Open Data ISTA Research Explorer

Sources

arXiv 2002.06465

Search this title in

Google Scholar