Library 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


 UsersGuideUser's Guide
 ExamplesLibrary of examples to demonstrate requirement definitions with package Modelica_Requirements
 VerifyLibrary of components to verify requirements
 TimeLocatorsLibrary of continuous time locators (output is true, if within time locator)
 ChecksInFixedWindowLibrary of check blocks (if the condition input is true, a property must hold)
 ChecksInFixedWindow_withFFTLibrary of check blocks that inspect properties in a fixed time window using FFT (Fast Fourier Transform)
 ChecksInSlidingWindowLibrary of check blocks that inspect a property in a sliding time window
 SignalAnalysisLibrary of signal analysis blocks to compute properties from Real signals
 LogicalFunctionsLibrary of logical functions (2-/3-valued logical operators without memory)
 LogicalBlocksLibrary of logical blocks (2-/3-valued logical operators with and without memory)
 SourcesLibrary of signal source blocks generating Real, Integer, Boolean and Property signals
 TypesLibrary of type definitions
 UtilitiesLibrary of utility functions
 InterfacesLibrary of interfaces and of partial blocks
 InternalLibrary of internal components (should not be directly used)

Generated at 2024-07-18T18:19:59Z by OpenModelicaOpenModelica 1.23.1 using GenerateDoc.mos