Assistance à la Certification d’Applications DIstribuées et Embarquées
Head : Philippe Queinnec
The ACADIE (Assistance to the Certification of Distributed and Embedded Applications) team studies the development and verification of critical software systems for which one has to exhibit a correctness certificate. The essence of such a certificate is a mathematical correctness proof. The ACADIE team studies how to elaborate such a certificate at three levels :
- At the fundamental level, the concepts of proof and computation are studied. The logical frameworks of Type Theory and Category Theory are considered.
- At the development level, we study the structuring concepts we need to put forward in order to make easier the production of correctness proofs. Moreover, we are interested in elaborating processes which produce software that is correct by construction. We address the Development of Critical Software.
- At the domain level, we address distributed real time systems and especially, critical embedded systems. Here, our concern is to understand the main abstractions and production processes of the domain in order to provide assistance to the Verification of Critical Distributed Systems.
The ACADIE team is structured accordingly in three groups :
Cette rubrique ne contient aucun article.