When designing complex and critical systems (planes, autonomous vehicles, etc.), it is crucial to be able to give guarantees that the system works as intended, which is often done through comprehensive testing. The goal of project BisoUS is to provide stronger guarantees, based on mathematics, and to detect problems as early as possible: solving them is then easier and cheaper.
Unfortunately this is a hard problem because some design choices may not have been done yet, and some key features (e. g. speed of a CPU) are then not known precisely enough.
In project BisoUS we develop formal methods, based on model-checking and synthesis to work with expressive modelling formalisms encompassing parameters, cost/rewards, and games on graphs to meet those challenges.