At Adfove, your privacy is important to us. This policy applies to all personal data we collect and describes how we collect, store, and use (together “Process”) such data. “Personal data” means any information relating to an identified or identifiable individual. It does not include data relating to a business or similar entity.
At Adfove, your privacy is important to us. This policy applies to all personal data we collect and describes how we collect, store, and use (together “Process”) such data. “Personal data” means any information relating to an identified or identifiable individual. It does not include data relating to a business or similar entity.
At Adfove, your privacy is important to us. This policy applies to all personal data we collect and describes how we collect, store, and use (together “Process”) such data. “Personal data” means any information relating to an identified or identifiable individual. It does not include data relating to a business or similar entity.
Products
Train Control System
Our train control system is developed in Event-B and TLA+ based on the described requirements for generating sequential code that runs on hardware. Our controller is modelised together with its concret environment in order to prove important safety properties at the system level for prevents derailments and collisions of trains.
Air Traffic Control Design Space Exploration Tool
Our tool will be useful for rapid Air Traffic Control design space exploration and verification at the system level, without resorting to detailed implementation and slow bit-level event-based simulation, it has well defined formal semantics, which facilitate bug avoidance using parametric and symbolic model checking and correct-by-construction.
DO-333 Qualification tool
Our qualification tool provide the evidence needed to demonstrate that the formal methods its within the scope of its intended use. The purpose of the qualification tool is to ensure that the tool provides confidence at least equivalent to that of the DO-178C processes which is eliminated, reduced, or automated.
A Framework for the Formal Verification of electric vehicle charging software
Our framework that takes charging control software and its requirements and outputs “yes”, if the control logic always fulfills the requirements, or otherwise “no” giving a counter example represented by a signal.We use the already existing tools :
-
Simulink Design Verifier (SLDV) for MathWorks’ Simulink software to find dead logic
-
Temporal Logic of Actions (TLA+) to defining timeout behavior and verifying time-sensitive in the communication between the Electric Vehicle and the Electric Vehicle Supply Equipment.