CONTROL SYSTEM ALGORITHMS VERIFICATION
Avocadi can verify control algorithms by automatic model checking, test case generation and model-based testing. Currently, Avocadi can verify algorithms programmed in FBD (Function Block Diagram) or SFC (Sequential Function Chart). Avocadi is primarily designed for safety PLCs but can also easily be used for non-safety I&C systems.
AUTOMATIC MODEL CHECKING WITH RELIABLE FORMAL REPRESENTATION
Avocadi provides automatic model checking of algorithms against specific customer requirements, ensuring the original requirements are not violated. Avocadi presents reliable functionally-equivalent formalisation, assuring the obtained model checking results can be automatically expected in the original algorithm.
TEST CASE GENERATION FOR MODEL-BASED TESTING
Avocadi provides deterministic methods for generating grey-box test cases according to the original algorithm. These test cases can be used for automatic MIL (Model In the Loop), SIL (Software In the Loop), and HIL (Hardware In the Loop) testing to verify that the final I&C system behaves similarly to the original algorithm.
REPRESENTATION OF VARIOUS CONTROL SYSTEMS
Avocadi utilises various libraries of function blocks to represent various control systems. A new library can be easily introduced for industrial or research purposes.
INTEGRATION INTO CURRENT DEVELOPMENT TOOLS
Avocadi can be easily integrated into the development tools of actual control systems. Such a control system allows users to significantly increase the reliability of their I&C systems by model checking or model-based testing.
EASIER QUALIFICATION OF SAFETY I&C SYSTEMS
The usage of Avocadi can be easily introduced into current development processes in the industry. This small change may lead to easier qualification of final I&C systems according to the strictest safety standards requiring the usage of formal methods and automatic testing.
What is AVOCADI?
What is Advanced Verification of Control Algorithm Design and Implementation?
AVOCADI is a stand-alone extensible tool capable of parsing and processing algorithms of various control systems into a model suitable for advanced verification. AVOCADI can perform reliable automatic model checking by functionally-equivalent formalization, calling a third-party model checker (NuSMV or nuXmv) and returning the model checking results. AVOCADI can also generate grey-box test cases and scenarios for MIL, SIL or HIL model-based testing to verify that the original algorithms are correctly implemented in the target simulation or PLC.
How AVOCADI works?
AVOCADI can parse control system algorithms provided in a supported format (e.g. JSON, REXYGEN model, Pertinax S project) and process them according to a selected library of function blocks (e.g. REX, ZAT, SJS). The list of supported formats can be easily expanded by programming an additional parser. AVOCADI also works with multiple libraries of prototyped function blocks, where each function block has its original definition, formal definition (for the formalisation) and definition of unit tests (for the test case generation methods). Once a prototyped block is defined in the library, it can be reused indefinitely. Each library can be iteratively extended to expand the set of supported types of blocks. A new library can be easily created for any new control system or special application. Finally, AVOCADI can be implemented directly into the development tools of a control system to provide users with even more intuitive tools for model-checking their algorithms.
FLEXIBLE INDUSTRIAL USAGE
Avocadi can currently be used on algorithms created in various IDEs, with the only restriction being that the algorithm must be modelled using FBD or SFC. This makes Avocadi suitable for many companies with their own IDE for designing control algorithms.
EXTENSIBLE BLOCKS LIBRARIES
For each specific control system or special application, custom libraries can be created by prototyping a block’s original definition, formal definition and definition of unit tests for each block from verified algorithms. These definitions are prototyped and verified only once. Then they can be reused indefinetely.
REASONABLE TEST CASE GENERATION
Avocadi generates test cases by combining predefined unit tests of function blocks used in the verified algorithm. Unit tests of each function block should ideally represent all its testable behaviour. When this condition is met, the presented method provides great robustness in creating test cases with the maximum reasonable coverage of the combined testable functionality of interconnected blocks.
ROBUST TEST SCENARIOS
Avocadi can translate generated test cases into test scenarios suitable even for HIL testing by a tester with an independent execution period if the tester is fast enough to provide the system’s input values, obtain the system’s output values and compare them with the expected output values. Avocadi is capable of generating scenarios in many formats and for various testers.
Contact us
Don’t hesitate to contact us at: tomasa@ntis.zcu.cz