Vers l'intégration de méthodes formelles dans le processus de développement de systèmes temps réel complexes

时间复杂性系统开发过程中的方法整合

基本信息

批准号：
238841-2011
负责人：
Boucheneb, Hanifa
金额：
$ 1.75万
依托单位：
École Polytechnique de Montréal
依托单位国家：
加拿大
项目类别：
Discovery Grants Program - Individual
财政年份：
2015
资助国家：
加拿大
起止时间：
2015-01-01 至 2016-12-31
项目状态：
已结题

来源：
https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=570505
关键词：
Vers int gration de thodes

项目摘要

La complexité grandissante et le caractère souvent critique des systèmes temps réel (systèmes de transport, systèmes de production, systèmes de communication, etc.) rendent indispensable une démarche de conception et de validation rigoureuse permettant d'en assurer la maîtrise, tout au long de leur cycle de vie. Les méthodes formelles, parce qu'elles s'appuient sur une base mathématique rigoureuse, sont largement reconnues comme étant une alternative incontournable pour développer des systèmes fiables. Cependant, l'intégration de ces méthodes dans les processus de développement dirigé par les modèles, utilisés en industrie, se heurte à plusieurs problèmes. Selon les concepteurs de systèmes, les méthodes formelles sont difficiles à comprendre et à appliquer, peu expressives, trop complexes ou mal adaptées aux besoins de spécifications. Par ailleurs, leurs techniques de vérification sont complexes, indécidables, souffrent du problème d'explosion combinatoire ou se limitent à des systèmes finis. Dans ce contexte, ce programme de recherche propose d'investiguer l'intégration de méthodes formelles dans le processus de développement de systèmes temps réel. Il vise, d'une part, à banaliser l'utilisation de ces méthodes en les enfouissant dans un processus de développement et, d'autre part, à parfaire et à étendre leur utilisation à des systèmes temps réel de plus en plus complexes. L'atteinte de ces objectifs généraux implique la réalisation des objectifs spécifiques suivants : 1) Établir / adapter / utiliser des techniques sûres de transformation de modèles de conception (UML, SysML, AADL, etc.) en modèles formels. 2) Concevoir et développer des techniques de model-checking ou de synthèse de contrôleur plus efficaces permettant une meilleure scalabilité que celles proposées dans la littérature. 3) Investiguer la combinaison de techniques de model-checking / synthèse de contrôleur et de preuve de théorème. 4) Implémenter, tester et valider les approches de vérification proposées.

La Complexité grandissante et le caractère souvent critique des systèmes temps réel（交通系统、生产系统、通讯系统等）生命周期。模型、应用开发过程中方法的集成在工业方面，请注意解决这些问题。 Il vise, d'une part, à banaliser l'utilization de ces关注具体对象的实现： 1) 概念模型（UML、SysML、AADL 等）转换模型的技术/适配器/利用者。 2) 构思和开发模型检查或综合控制技术以及文学中建议的最佳可扩展性的效果。 3) 调查模型检查技术/控制综合技术与理论预演的组合。 4) 实施、测试和验证验证提案的方法。