A formal refinement framework for the systems modeling language
<p>The Systems Modeling Language (SysML), an extension of a subset of the Unified Modeling Language (UML), is a visual modelling language for systems engineering applications. At present, the semi-formal SysML, which is widely utilised for the design of complex heterogeneous systems, lacks int...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2015
|
| Subjects: |
| _version_ | 1797080952033247232 |
|---|---|
| author | Jacobs, P |
| author2 | Simpson, A |
| author_facet | Simpson, A Jacobs, P |
| author_sort | Jacobs, P |
| collection | OXFORD |
| description | <p>The Systems Modeling Language (SysML), an extension of a subset of the Unified Modeling Language (UML), is a visual modelling language for systems engineering applications. At present, the semi-formal SysML, which is widely utilised for the design of complex heterogeneous systems, lacks integration with other more formal approaches. In this thesis, we describe how Communicating Sequential Processes (CSP) and its associated refinement checker, Failures Divergences Refinement (FDR), may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We do so by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities, state machines and interactions are given a formal process-algebraic semantics. These behaviours execute within the context of the structural diagrams to which they relate, and this is reflected in the CSP descriptions that depict their characteristic patterns of interaction. The resulting abstraction gives rise to a framework that enables the formal treatment of integrated behaviours via refinement checking. In SysML, requirement diagrams allow for the allocation of behavioural features in order to present a more detailed description of a captured requirement. Moreover, we demonstrate that, by providing a common basis for behaviours and requirements, the approach supports requirements traceability: SysML requirements are amenable to formal verification using FDR. In addition, the proposed framework is able to detect inconsistencies that arise due to the multi-view nature of SysML. We illustrate and validate the contribution by applying our methodology to a safety critical system of moderate size and complexity.</p> |
| first_indexed | 2024-03-07T01:07:38Z |
| format | Thesis |
| id | oxford-uuid:8be42735-8a31-41e2-82e2-05f7d0e6cb1a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T01:07:38Z |
| publishDate | 2015 |
| record_format | dspace |
| spelling | oxford-uuid:8be42735-8a31-41e2-82e2-05f7d0e6cb1a2022-03-26T22:41:03ZA formal refinement framework for the systems modeling languageThesishttp://purl.org/coar/resource_type/c_db06uuid:8be42735-8a31-41e2-82e2-05f7d0e6cb1aFormal methods (Computer science)Computer scienceCSP (Computer program language)SysML (Computer science)EnglishORA Deposit2015Jacobs, PSimpson, ACavarra, AEarle, C<p>The Systems Modeling Language (SysML), an extension of a subset of the Unified Modeling Language (UML), is a visual modelling language for systems engineering applications. At present, the semi-formal SysML, which is widely utilised for the design of complex heterogeneous systems, lacks integration with other more formal approaches. In this thesis, we describe how Communicating Sequential Processes (CSP) and its associated refinement checker, Failures Divergences Refinement (FDR), may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We do so by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities, state machines and interactions are given a formal process-algebraic semantics. These behaviours execute within the context of the structural diagrams to which they relate, and this is reflected in the CSP descriptions that depict their characteristic patterns of interaction. The resulting abstraction gives rise to a framework that enables the formal treatment of integrated behaviours via refinement checking. In SysML, requirement diagrams allow for the allocation of behavioural features in order to present a more detailed description of a captured requirement. Moreover, we demonstrate that, by providing a common basis for behaviours and requirements, the approach supports requirements traceability: SysML requirements are amenable to formal verification using FDR. In addition, the proposed framework is able to detect inconsistencies that arise due to the multi-view nature of SysML. We illustrate and validate the contribution by applying our methodology to a safety critical system of moderate size and complexity.</p> |
| spellingShingle | Formal methods (Computer science) Computer science CSP (Computer program language) SysML (Computer science) Jacobs, P A formal refinement framework for the systems modeling language |
| title | A formal refinement framework for the systems modeling language |
| title_full | A formal refinement framework for the systems modeling language |
| title_fullStr | A formal refinement framework for the systems modeling language |
| title_full_unstemmed | A formal refinement framework for the systems modeling language |
| title_short | A formal refinement framework for the systems modeling language |
| title_sort | formal refinement framework for the systems modeling language |
| topic | Formal methods (Computer science) Computer science CSP (Computer program language) SysML (Computer science) |
| work_keys_str_mv | AT jacobsp aformalrefinementframeworkforthesystemsmodelinglanguage AT jacobsp formalrefinementframeworkforthesystemsmodelinglanguage |