Sökning: id:"swepub:oai:DiVA.org:kth-290846" >
Formally Proving Co...
Formally Proving Compositionality in Industrial Systems with Informal Specifications
-
- Nyberg, Mattias (författare)
- KTH,Mekatronik
-
- Westman, Jonas, 1986- (författare)
- KTH,Mekatronik
-
- Gurov, Dilian, 1964- (författare)
- KTH,Teoretisk datalogi, TCS
-
(creator_code:org_t)
- 2020-10-27
- 2020
- Engelska.
-
Ingår i: ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Applications. - Cham : Springer Science and Business Media Deutschland GmbH. ; , s. 348-365
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- Based upon first-order logic, the paper presents a methodology and a deductive system for proving compositionality. Typical specifications found in industry are not expressed in any formal notation; rather most often in natural language. Therefore, the methodology does not assume specifications to be formal logical sentences. Instead, the methodology takes as input, properties of specifications and in particular, refinement relations. To cover general industrial heterogeneous systems, the semantics chosen is behavior based, originating in previous work on contract-based design for cyber-physical systems. In contrast to the previous work, implementation of specifications is non-monotonic with respect to composition. That is, even though a specification is implemented by one component, a composition with a second component may not implement the same specification. This kind of non-monotonicity is fundamentally important to support architectural specifications and so-called freedom-of-interference used in design of safety critical systems.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- Embedded systems
- Formal logic
- Formal methods
- Safety engineering
- Semantics
- Architectural specifications
- Contract-based designs
- Deductive systems
- First order logic
- Heterogeneous systems
- Industrial systems
- Natural languages
- Safety critical systems
- Specifications
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)