kth.sePublications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formally Proving Compositionality in Industrial Systems with Informal Specifications
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.ORCID iD: 0000-0001-6667-3783
KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.ORCID iD: 0000-0002-9655-7326
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-0074-8786
2020 (English)In: ISoLA 2020: Leveraging Applications of Formal Methods, Verification and Validation: Applications, Springer Science and Business Media Deutschland GmbH , 2020, p. 348-365Conference paper, Published paper (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH , 2020. p. 348-365
Series
Lecture Notes in Computer Science book series ; 12478
Keywords [en]
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
National Category
Computer and Information Sciences
Identifiers
URN: urn:nbn:se:kth:diva-290846DOI: 10.1007/978-3-030-61467-6_22Scopus ID: 2-s2.0-85096474754OAI: oai:DiVA.org:kth-290846DiVA, id: diva2:1539204
Conference
International Symposium on Leveraging Applications of Formal Methods, 20 October 2020 through 30 October 2020
Note

QC 20210323

Available from: 2021-03-23 Created: 2021-03-23 Last updated: 2023-03-27Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Nyberg, MattiasWestman, JonasGurov, Dilian

Search in DiVA

By author/editor
Nyberg, MattiasWestman, JonasGurov, Dilian
By organisation
MechatronicsTheoretical Computer Science, TCS
Computer and Information Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 196 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf