Full Text Available
Note: Clicking the button above will open the full text document at the original institutional repository in a new window.
A new dialect of SOFL-Syntax formal semantics and tool support
Dissertation (MSc)--University of Pretoria, 2018.
Saved in:
| Other Authors: | |
|---|---|
| Format: | Thesis |
| Published: |
University of Pretoria
2019
|
| Subjects: | |
| Tags: |
No Tags, Be the first to tag this record!
|
| _version_ | 1867613465681592320 |
|---|---|
| access_status_str | Open Access |
| author2 | Gruner, Stefan |
| author_browse | Gruner, Stefan |
| author_facet | Gruner, Stefan |
| collection | Thesis |
| dc_rights_str_mv | © 2019 University of Pretoria. All rights reserved. The copyright in this work vests in the University of Pretoria. No part of this work may be reproduced or transmitted in any form or by any means, without the prior written permission of the University of Pretoria. |
| description | Dissertation (MSc)--University of Pretoria, 2018. |
| format | Thesis |
| id | oai:repository.up.ac.za:2263/72706 |
| institution | University of Pretoria (South Africa) |
| last_indexed | 2026-06-10T12:36:34.949Z |
| license_str | Other — see source repository |
| provenance_str_mv | Harvested via OAI-PMH from UPSpace — University of Pretoria Institutional Repository |
| publishDate | 2019 |
| publishDateRange | 2019 |
| publishDateSort | 2019 |
| publisher | University of Pretoria |
| publisherStr | University of Pretoria |
| record_format | dspace |
| source_str | UPSpace — University of Pretoria Institutional Repository |
| spelling | oai:repository.up.ac.za:2263/72706 A new dialect of SOFL-Syntax formal semantics and tool support Gruner, Stefan u97016889@tuks.co.za van der Berg, Johan Sarel UCTD Process algebra Formal modeling Formal semantics mCRL2 Restricted dialect SMT-Solver Structured Object Orientated Formal Language Tool support Engineering, built environment and information technology theses SDG-09 Dissertation (MSc)--University of Pretoria, 2018. Structured Object Orientated Formal Language (SOFL) is a formal method design methodology that combines data flows diagrams and predicates in order to describe processes that can be refined. This methodology creates a very versatile method of describing a system, which system properties can be proven rigorously. Data flows are grouped by ports that define from which data flows data can be consumed or on which flows data can be generated. For predicates, Logic of Partial Functions (LFP) are used; and an undefined element that is also used to indicate if a data flows do not contain any data. Over time SOFL “evolved organically” and a number of features were added: usability was the main consideration for a feature being added. For a formal language to be useful there must be no uncertainty of a specific design’s meaning. With SOFL, there is a possible contradiction between the requirement that a process's precondition must be true when the process fire, and the fire rules. This contradiction is due to the use of LPF. Semantics (the meaning) of SOFL was not always updated to keep track of the changes made to SOFL which resulted in an outdated and incomplete semantic. The incompleteness of the semantics is a significant factor motivating the work done in this dissertation. In this dissertation, a dialect of SOFL is created to define a semantic. Not all the elements of SOFL are added in order that a simpler semantic can be defined. Elements that were removed include: LPF, Classes, and Non-deterministic broadcast nodes. Semantics of the dialect is created by a two-step process: firstly, an intuitive understanding of the dialect is created, and secondly, both static and dynamic semantics are defined by means of translations. A translation is a mapping from the dialect to a formal language that describes a certain aspect of the dialect. Static semantics defines the meaning of the elements that are “fixed” in their state: SMT-LIB is used as the target language to describe the static semantics of the dialect. Dynamic semantics describes how an element in a design changes over time: the process algebra mCRL2 is used as the formal language which describes the dynamic behaviour of the dialect. The SMT-Solver Z3 and tools included in mCLR2 are used to analyse the translation of the dialect. Use of these tools allows properties that are necessary for a design to have a well defined meaning, to be proven. Properties that can be proven include: a process can fire, a process can fire an infinite number of times, and a predicate that described a property. An Eclipse plug-in is created so that translation is not required to be done manually. After a design is translated the tools Z3 and mCRL2 are run using script files and the results of the analysis are displayed on the screen. The desired properties could be proven but for a moderate size design, but as the size of the design increased the analysis of the translation could not be completed due to computational problem. Usability of the tool can be improved by not only using a textual representation of a design, but also visual representations as in SOFL. As a result, properties that are necessary for a design to have a well-defined meaning, can be proven using these tools. bs2026 Computer Science MSc Unrestricted SDG-09: Industry, innovation and infrastructure 2019-12-13T08:07:43Z 2019-12-13T08:07:43Z 2019/09/03 2018 Dissertation van der Berg, JS 2018, A new dialect of SOFL-Syntax formal semantics and tool support, MSc Dissertation, University of Pretoria, Pretoria, viewed yymmdd <http://hdl.handle.net/2263/72706> S2019 http://hdl.handle.net/2263/72706 © 2019 University of Pretoria. All rights reserved. The copyright in this work vests in the University of Pretoria. No part of this work may be reproduced or transmitted in any form or by any means, without the prior written permission of the University of Pretoria. application/pdf University of Pretoria |
| spellingShingle | UCTD Process algebra Formal modeling Formal semantics mCRL2 Restricted dialect SMT-Solver Structured Object Orientated Formal Language Tool support Engineering, built environment and information technology theses SDG-09 A new dialect of SOFL-Syntax formal semantics and tool support |
| title | A new dialect of SOFL-Syntax formal semantics and tool support |
| title_full | A new dialect of SOFL-Syntax formal semantics and tool support |
| title_fullStr | A new dialect of SOFL-Syntax formal semantics and tool support |
| title_full_unstemmed | A new dialect of SOFL-Syntax formal semantics and tool support |
| title_short | A new dialect of SOFL-Syntax formal semantics and tool support |
| title_sort | new dialect of sofl syntax formal semantics and tool support |
| topic | UCTD Process algebra Formal modeling Formal semantics mCRL2 Restricted dialect SMT-Solver Structured Object Orientated Formal Language Tool support Engineering, built environment and information technology theses SDG-09 |
| url | http://hdl.handle.net/2263/72706 |