Building Trustworthy Software with the Power of AI
At Verum, we support engineers to build highly reliable software faster using a specialized branch of Artificial Intelligence known as symbolic AI (AKA formal methods). This is crucial for safety- and mission-critical systems — such as those in automotive, semiconductor manufacturing, and medical devices — where errors are simply not an option.
Verum’s model-based engineering tools allow engineers to:
- Design software through models with visual support.
- Simulate system behavior to detect issues early.
- Verify software mathematically rigorously to ensure correctness under all conditions.
- Automatically generate high-quality code in C++, C#, C, Python, and JavaScript.
Rather than manually coding thousands of lines and fixing bugs afterward, engineers use Verum’s tooling to create reliable software models and automatically generate clean, reliable code, which saves time and reduces risks.
Verum’s technology is used to design and build complex, dependable software systems.
Cynergy4MIE
Together with the Eindhoven University of Technology (TU/e) steps are made to advance the technology together with experimenting with approaches to make these technologies easier accessible for larger audiences.
The following research domains are jointly researched with TU/e:
- The software engineer uses a Verum developed domain specific language (DSL), to design the structure and behavior of a software system with a syntax similar to that of common programming languages such as Java or C. It allows to generate directly deployable code such as C, C++ and C#. In Cynergy4MIE, the expressiveness of the DSL is expanded. Example of essential enhancements that will be worked on in Cynergy4MIE are:
- Incorporating invariants to enable automated traceability of requirements, allowing the development organization to confirm that implementations align correctly with specifications. The verification and validation tools then furnish users with formal proofs of compliance.
- Lifting the verification to a system level (components of components) by adding functional system requirements using an aspect oriented way for specifying and verifying safety and liveness properties.
- Addition of specification of fairness properties and the verification of these eliminating some, current unavoidable, false positives and extending the family of liveness properties to be specified and checked.
- Addition of global (external) functions connecting handwritten (library) calls removing the need for additional helper ports. For verification of non-void external function calls, all possible return values are considered and verified.
- TU/e is supporting a model checker called mCRL2, which is a specification language for describing concurrent discrete event systems. It is accompanied with a toolset, that facilitates tools, techniques and methods for simulation, analysis and visualization of behavior. The behavioral part of the language is based on process algebra. Verum’s work is tightly integrated with mCRL2: the model checker is applied to mathematically verify the specifications made in the DSL. When the expressiveness of the DSL is expanded, mCRL2 must comply with it:
- Improvements of the connection with the mCRL2 tooling and new ways of state space generation of mCRL2 tooling itself increasing the maximal state space to be handled. Hereby fundamentally extending the applicability of this development method.
- Another research group at TU/e is scoping a low-code platform on the basis of Verum’s DSL that empowers domain experts with little software background to develop and deploy formally verified embedded software focused on robotics. This platform should allow experts to focus on what the system should do, while correctness, consistency, and deployability are ensured automatically. Verum is supporting TU/e with adding functions related to microservices to the DSL:
- Enhancements to service oriented or microservices architectures, demonstrated by employing ROS 2 as the middleware and execution platform.
From concept to demonstrator
The current work focuses on creating the fundaments on which a demonstrator will be built. The low code platform supported by the advancements in technology will showcase a revolutionary paradigm in creating software in the domain of advanced robotics: software created by non-software engineers, increased productivity and the highest code correctness possible.
Blog signed by: Verum team