Skip to main content

Notice: this Wiki will be going read only early in 2024 and edits will no longer be possible. Please see: https://gitlab.eclipse.org/eclipsefdn/helpdesk/-/wikis/Wiki-shutdown-plan for the plan.

Jump to: navigation, search

Eclipse 4diacWiki/Development/Modeling Implicit Assumptions

Overview page of GSoC 2023 Project

The aim of this project is to provide better infrastructure for observation and early error detection of modern automation systems, with inspiration from contract-based design (CBD).

Topic

Eclipse 4diac: Modeling Implicit Assumptions within IEC 61499 Software

Project Goals

Automated software engineering helps developers of control software to manage complex industrial applications. Eclipse 4diac has, in recent years, advanced in terms of providing tool support for domain experts. The control software is typically executed in real-time and distributed across devices. To detect faults early, modeling implicit assumptions within IEC 61499 software can provide the basis for automated checks. A key goal of the project is to deliver tools for creation and evaluation of such assumptions described in a contract specification language. Where user interactions are required, graphical visualizations are provided.

Milestones

Implementation Plan and Concept in 4diac IDE

CBD was already discussed in a lot of literature but no implementation in 4diac IDE, so the following implementation was chosen. A contract consists of Contract Elements that follow a specification language. All implementations were created in a dedicated plug-in in 4diac IDE.

Decided on the following syntax for Contract Elements:

  • ASSUMPTION EVENT occurs every TIMEms
  • ASSUMPTION EVENT occurs every TIMEms with TIMEms offset
  • GUARANTEE Whenever EVENT occurs, then event EVENT occurs within TIMEms
  • GUARANTEE Reaction (EVENT,EVENT) within TIMEms
  • GUARANTEE Whenever event EVENT occurs, then events (EVENT,EVENT) occur within TIMEms

EVENT is replaced by a user-selected event pin. TIME is replaced by a user input, i.e., an instant (such as "7") or an interval (such as "[7,9]")

A menu entry and dialogues for user interaction to create a contract were needed. The contract data needed to be stored so that no major rewrite of existing models is needed. The user only sees the Contract. All the evaluation and simplification is done in an IEC 61499 model in the backend of 4diac IDE without additional inputs except for the contract that was specified by the user.

Implementation Steps

Input Dialog

Manually recording the contract in a specific language for defining contracts needs an understanding of the language and an exact sequence of characters because a wrong space leads to a invalid contract. Dialog windows were integrated into 4diac IDE to help the user generate correct contracts. For every Contract Element, a dialog was implemented. The following screenshot shows the dialog window for creating an Assumption. Similar dialogs were created for guarantees (depending on the selection, the version for 1 or 2 output pins is shown) and reactions. Assumptions can have an optional offset that can be selected by the user.


Eclipse4diac gsoc2023 dialog.PNG


(Commits 204206, 203447 , 203488, 203587, 203653, 203718, 204012, 203659, 204014, 204160, 204161, 204167, 204546 )

Contract Model

The Contract is visualized as the comment of a SubApp with a name starting with _Contract. This implementation was used because the contract should be visible by the user and stored in a standard-compliant format. The implementation also uses already existing models (i.e., SubApps) and does not interfere with any already existing systems. The contract model builds a core of classes that describe the elements of a contract. Instances of these classes can form a representation of a contract. The essential parts of the contract are extracted by helper classes from a String that is provided by the user via the implemented dialog. The contract model uses its own time classes to represent an Instant or an Interval. The representation allows to provide helper methods for managing time slots, such as the overlap between two intervals, or to check whether an instant is contained in an interval. This helps to efficiently check the validity of a contract. (Commits 204154, 204249 , 204313, 204450)

The next figure shows an example for a contract defined over an FB:

Eclipse4diac gsoc2023 examplecontract.PNG

a) Contract Elements All elements that can belong to a contract are derived from the abstract ContractElement class. A ContractElement holds a time, input event and a contract and implements getters and setters for private fields. It also forces all non abstract subclasses to implement isValid() and asString(). All subclasses have factory methods for creating an object of the respective class from Strings that are provided in a contract specification language.

a.1) Assumptions focus on an input event pin. Software developers can specify how often this event occurs (e.g., every 5ms / within [5,7]ms). Assumptions are the elements of the contract that pose restrictions on the occurrence of the input events that are a part of the contract. All inherited abstract functions are implemented and some additional functions that are used for evaluating the whole contract. For instance, it offers methods for checking whether an Assumption is valid. An Assumption with offset holds an additional time parameter.

a.2) Guarantees focus on output event pins. Guarantees are the elements that guarantee properties for the occurrence of output events defined in the Contract as long as the contract is Valid and the Assumption of the Contract hold. There are different possible Guarantees for a contract, which are all realized as subclasses of contract elements.

  • a.2.1) Guarantee: After a specific input Event an Output event is guaranteed. Only has an additional field for the OutputEvent and the Getters/setters for it.
  • a.2.2) Reaction: After a specific input Event an Output event for the specific input Event is guaranteed.Only has an additional field for the OutputEvent and the Getters/setters for it. Reaction extends Guarantee.
  • a.2.3) Guarantee for two OutputEvents is realized as a separate class that extends Guarantee. After a specific input event, the occurrence of two OutputEvents for the input Event is guaranteed. The class provides two additional fields for the two output events and the corresponding getters/setters.

All Guarantees implement all their inherited abstract functionality and some additional functions that are used when evaluating the whole contract.


b) Contracts hold a list of assumptions and a list of guarantees. Additionally, each contract holds a reference to an FBNetworkElement (the owner of the contract), Optional<String> for collecting any potential error of the contract, and a ContractState. ContractState is internally used. For all others fields, the Contract class provides Getters/Setters and methods for adding/removing. The contract also has a method writeToOwner() that writes the contract as comment to the SubApp owner. getAsString() returns the contract as a string that is compliant with the specification language. isValid() checks whether the contract is valid. The contract is valid when it is consistent in itself, and when there is an Assumption-Guarantee pair. The evaluation only recognizes a basic set of errors at this point. The corresponding logic needs to be expanded upon in the future to evaluate more complex contracts. The factory method getContractFromComment is used to create a new contract from a String (which can be the comment of a subapp). This is used when loading a contract from a project that exists as an XML file. (Commits [1])

Eclipse4diac gsoc2023 validcontract.PNG

c) Contract Exceptions

The Contract Model has its own Exceptions with a field to store the contract or the contract element where the exception occurred. Different kinds of exception were implemented, which represent different kinds of errors that can occur. All exceptions inherit from a generic ContractException class.

(Commits 204112, 204349, 204449)


Commits The implementation of the model was fluid and was reworked while implementation. There is no clear separation possible for the commits for ContractElements and the contract itself. (Commits 203683,204015,204023,204065,204102,204152,204207,204254, 204275,204262,204352,204356,204356,204397,204465,204484 )


Model Tests

Tests for the Contract Model are implemented to validate their correctness. The are realized as Junit tests and included in the tests of the model plugin (Commit 204466). They test, among other things, the following aspects:

  • whether the Strings representing the Contract Elements are correctly imported and the model is created correctly. Based on this model, it is validated whether the information is correctly transcribed into a String again.

(Commits 204355, 204390, 204393, 204364)

  • whether two Contract Elements that work on the same Events are simplified correctly

(Commits 204401, 204394)

  • whether the validation of the contract is correct regarding evaluating the consistency of a contract

(Commits 204390, 204408)


Not merged

Not all improvement proposals were merged. As the contract is stored as a comment, it can be currently edited by hand. Removing the possibility of editing contracts by hand fixes this. However, the stakeholders were uncertain whether a manual editing is required. The commit can be merged at any time if needed. Commit 203558


Related Work

During the work on this project, also infrastructure from other plug-ins was extended or improved.

Final Report (Summary)

In this Google Summer of Code-project, the infrastructure for CBD was added directly in the IDE. 4diac IDE now supports a specification language for the creation of contracts. This includes an internal model to handle the contract and its elements. As is common for projects that need to work well with an already existing code base, extra care was given to integrate the basic function of CBD without limiting its extensibility with other functions of 4diac IDE and without interfering with these functions. CBD can serve as a powerful new infrastructure for 4diac IDE in the future that has much room to expand the capabilities of 4diac IDE. As a result, some of the topics (e.g., the interaction of different contracts) could not be analyzed in-depth, yet a working prototype demonstrating the basic concept is available as part of Eclipse 4diac. Furthermore, the implemented test cases demonstrate how to use the provided infrastructure. Stakeholders who may use the tooling in the future were contacted regularly to gather their requirements. User wishes were driving the implementations and resulted in a number of changes in the newly implemented code along the way, thus, adapting the implementation to user needs. All the deliverables described in the project proposal were merged into the 4diac IDE repository.

A list of all my commits is available under the following link: Gerrit

Back to the top