FORMAL REPRESENTATION
A formal representation for a given customer algorithm, completely tailor-made. Essentially, it is a formal digital twin that is then used by the Avocadi tool.
MODEL CHECKING
Avocadi can implement a model checking for customer specific algorithm checking based on specific customer requirements, ensuring that the original requirements are not violated.
TEST GENERATION
Unique creation of unit tests for a customer library of blocks which are subsequently used to generate tests of the entire original algorithm.
What is AVOCADI?
What is Advanced Verification of Control Algorithm Design and Implementation?
AVOCADI is a stand-alone extensible tool capable of parsing an original model from some source file, generating a functionally-equivalent formalized model, calling a third-party model checker (NuSMV or nuXmv) and returning the model checking results. AVOCADI can also be used to generate grey-box test cases and scenarios for MIL, SIL or HIL testing of the original FBD algorithm. Furthermore, Avocadi provides various support functions for verification, analysis, self-testing, and MIL testing.
How AVOCADI works?
AVOCADI can parse FBD algorithms in supported source file formats. Nevertheless, it can be extended to support a new source file format 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.
FLEXIBLE USAGE
Avocadi can currently be used on a model created in any IDE with the only restriction that the algorithm must be modeled using FBD. This makes Avocadi suitable for a large number of companies that have their own IDE for creating algorithms.
FLEXIBLE BLOCKS LIBRARY
For each specific company, custom formal libraries can be created, which are then used by the Avocadi tool. This fact provides great flexibility in the use of the Avocadi tool.
FLEXIBLE UNIT TESTS REPRESENTATION
For each functional block in a customer library, unit tests can be built using a unique method. This method provides great robustness in creating unit tests with the maximum possible coverage of the functionality of a given block. These unit tests are then used in Avocadi to generate tests for the entire algorithm.
FLEXIBLE TESTING SCENARIO
Avocadi can automatically build test scenarios for the selected algorithm thanks to the created set of unique unit tests. These tests can then be used for MIL, SIL, HIL testing, but also for validation on the target device using the test platform. This greatly streamlines the overall testing process.
Our Team
- Tomáš Ausberger
- Karel Kubíček
- Pavla Medvecová
Contact us
If you are interested in the possibilities of the Avocadi tool, do not hesitate to contact us.
Contact usContact form will be displayed here. To activate it you have to set the "contact form shortcode" parameter in Customizer.