We present a graphical toolset for verifying AADL models, which are gaining widespread acceptance in aerospace, automobile and avionics industries for comprehensively specifying safety-critical systems by capturing functional, probabilistic and hybrid aspects. Analyses are implemented on top of mature model checking tools and range from requirements validation to functional verification, safety assessment...
In this paper we present Pessoa, a tool for the synthesis of correct-by-design embedded control software. Pessoa relies on recent results on approximate abstractions of control systems to reduce the synthesis of control software to the synthesis of reactive controllers for finite-state models. We describe the capabilities of Pessoa and illustrate them through an example.
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.