.Modelica_Requirements .Modelica_RequirementsLibrary Modelica_Requirements is a Modelica package to formally define requirements and checking them automatically when a model is simulated. An overview of this library is given in the publication Formal Requirements Modeling for Simulation-Based Verification
In order to define properties and requirements mostly a 2-valued logic is used. There are some functions and blocks based on 3-valued logic using type Property, especially block Requirement. Furthermore, there are cast-operators to map 2-valued to 3-valued logic and vice versa. 3-valued logic is used to define (a) if a property is not tested (because only relevant in a certain situation) and (b) if a requirement was not tested in a simulation run.
In this package the standard convention is used that names of memory-less operators (implemented as Modelica functions) start with lower-case letters and names of operators with memory (implemented as Modelica blocks) start with upper-case letters.
This package uses basically Modelica 3.2 language elements and requires at least version 3.2.2 of the Modelica Standard Library (some parts will not work with 3.2.1 or an earlier version). Additionally, the Modelica extension is used in some examples (but not outside of examples) to pass a model instance as argument to a function (and the function argument is a record). This feature is used to associate requirements in a reasonably convenient way with behavioral models. This approach is currently under discussion at the Modelica Association. Most likely a slightly different concept will be introduced in the next release of the Modelica language by providing the cast of a model to a record. Once this is clear and prototypes are available in Modelica tools, this new concept will be used in this library. Earlier versions of this library contained also examples utilizing the proposed new Modelica language element to "call a block as a function". These examples had been removed from this version.
The current version of the library uses a buffer for the implementation of sliding windows (Internal.SlidingWindow). The size of this buffer is fixed to 20 (constant nBuffer in package SlidingWindow). If the buffer is too small for a requirement from package ChecksInSlidingWindow, then a warning is printed. The result of the requirement verification might then not be correct.
This package is not yet finalized. A redesign is planned. The redesigned library (with improved implementations of models and new functionality) should be backwards compatible to this version, but it is not guaranteed. If non-backwards compatible changes are introduced, most likely automatic conversions will not be provided..
This Modelica package is free software and the use is completely at your own risk; it can be redistributed and/or modified under the terms of the Modelica license 2, see the license conditions (including the disclaimer of warranty) at https://www.Modelica.org/licenses/ModelicaLicense2.
Copyright © 2014-2016, DLR, Dassault Aviation and UNICAL
| Name | Description |
|---|---|
 UsersGuide | User's Guide |
 Examples | Library of examples to demonstrate requirement definitions with package Modelica_Requirements |
 Verify | Library of components to verify requirements |
 TimeLocators | Library of continuous time locators (output is true, if within time locator) |
 ChecksInFixedWindow | Library of check blocks (if the condition input is true, a property must hold) |
 ChecksInFixedWindow_withFFT | Library of check blocks that inspect properties in a fixed time window using FFT (Fast Fourier Transform) |
 ChecksInSlidingWindow | Library of check blocks that inspect a property in a sliding time window |
 SignalAnalysis | Library of signal analysis blocks to compute properties from Real signals |
 LogicalFunctions | Library of logical functions (2-/3-valued logical operators without memory) |
 LogicalBlocks | Library of logical blocks (2-/3-valued logical operators with and without memory) |
 Sources | Library of signal source blocks generating Real, Integer, Boolean and Property signals |
 Types | Library of type definitions |
 Utilities | Library of utility functions |
 Interfaces | Library of interfaces and of partial blocks |
 Internal | Library of internal components (should not be directly used) |