View in EDS PDF Full Text

On the formal interpretation and behavioural consistency checking of SysML blocks.

Saved in:
Bibliographic Details
Title: On the formal interpretation and behavioural consistency checking of SysML blocks.
Authors: Jacobs, Jaco1 Jaco.Jaobs@cs.ox.ac.uk, Simpson, Andrew1 Andrew.Simpson@cs.ox.ac.uk
Source: Software & Systems Modeling. Oct2017, Vol. 16 Issue 4, p1145-1178. 34p.
Subjects: SysML (Computer science), Computer software development, Software productivity, Software engineering, Electronic data processing, Information science
Abstract: The Systems Modeling Language (SysML) is a semi-formal, graphical modelling language used in the specification and design of systems. We describe how Communicating Sequential Processes (CSP) and its associated refinement checker, FDR3, may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We achieve this by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities and state machines 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. We describe how CSP and FDR3 can be used in conjunction with SysML in a formal, top-down approach to systems engineering. Moreover, the compositionality afforded by CSP alleviates the state space explosion problem frequently encountered with complex formal models and complements the top-down approach of SysML. Typically, a system is composed from constituent systems using the concept of blocks. SysML permits two alternative interpretations with regard to the behaviour of the resulting composition. We argue that the use of a process-algebraic formalism enables us to explore the relationships between these interpretations in a more rigorous fashion than would otherwise be the case. [ABSTRACT FROM AUTHOR]
Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 125293206
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: On the formal interpretation and behavioural consistency checking of SysML blocks.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Jacobs%2C+Jaco%22">Jacobs, Jaco</searchLink><relatesTo>1</relatesTo><i> Jaco.Jaobs@cs.ox.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Simpson%2C+Andrew%22">Simpson, Andrew</searchLink><relatesTo>1</relatesTo><i> Andrew.Simpson@cs.ox.ac.uk</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Software+%26+Systems+Modeling%22">Software & Systems Modeling</searchLink>. Oct2017, Vol. 16 Issue 4, p1145-1178. 34p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22SysML+%28Computer+science%29%22">SysML (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+development%22">Computer software development</searchLink><br /><searchLink fieldCode="DE" term="%22Software+productivity%22">Software productivity</searchLink><br /><searchLink fieldCode="DE" term="%22Software+engineering%22">Software engineering</searchLink><br /><searchLink fieldCode="DE" term="%22Electronic+data+processing%22">Electronic data processing</searchLink><br /><searchLink fieldCode="DE" term="%22Information+science%22">Information science</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: The Systems Modeling Language (SysML) is a semi-formal, graphical modelling language used in the specification and design of systems. We describe how Communicating Sequential Processes (CSP) and its associated refinement checker, FDR3, may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We achieve this by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities and state machines 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. We describe how CSP and FDR3 can be used in conjunction with SysML in a formal, top-down approach to systems engineering. Moreover, the compositionality afforded by CSP alleviates the state space explosion problem frequently encountered with complex formal models and complements the top-down approach of SysML. Typically, a system is composed from constituent systems using the concept of blocks. SysML permits two alternative interpretations with regard to the behaviour of the resulting composition. We argue that the use of a process-algebraic formalism enables us to explore the relationships between these interpretations in a more rigorous fashion than would otherwise be the case. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Software & Systems Modeling is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=125293206
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10270-015-0511-z
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 34
        StartPage: 1145
    Subjects:
      – SubjectFull: SysML (Computer science)
        Type: general
      – SubjectFull: Computer software development
        Type: general
      – SubjectFull: Software productivity
        Type: general
      – SubjectFull: Software engineering
        Type: general
      – SubjectFull: Electronic data processing
        Type: general
      – SubjectFull: Information science
        Type: general
    Titles:
      – TitleFull: On the formal interpretation and behavioural consistency checking of SysML blocks.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Jacobs, Jaco
      – PersonEntity:
          Name:
            NameFull: Simpson, Andrew
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 10
              Text: Oct2017
              Type: published
              Y: 2017
          Identifiers:
            – Type: issn-print
              Value: 16191366
          Numbering:
            – Type: volume
              Value: 16
            – Type: issue
              Value: 4
          Titles:
            – TitleFull: Software & Systems Modeling
              Type: main
ResultId 1