依赖性驱动的DiaSuite：设计和实施安全软件应用程序的方法

从Fo rmation到Doctorale再到informaticEDMIB或Rdeaux的控制或管理学校订单号安全运行的软件应用程序的升级一个aprochedirigeepar的概念他们是于2013年5月6日获得支持Doctorat的大学（specialiteinformatique）通过昆汀·埃纳尔陪审团PR居民：穆罕默德·莫斯巴，B o rdeaux P奥林匹克技术学院教授报告员：克里斯托弗·多尼马克-奥利维尔·基利吉安Mont p Ellier大学教授I我在图卢兹LAAS-CNRS研究中心工作检查员：查尔斯·康塞尔尼古拉斯·洛里昂Professeur'在P奥林匹克理工学院的BordeauxResearchAsociate'在一个A B S T R A CTdEVElopMEnTOFDEpEndAb eApplICATIOns：A从S.I.G. N-D河N A.P.罗奇在许多领域，如航空电子、医疗或家庭自动化，软件应用程序发挥着越来越重要的作用，甚至可能对其环境至关重要。为了信任这些应用程序，它们的开发受到依赖性要求的约束。然而，有必要证明，在整个开发周期中，这些高级别要求都得到了考虑，并实施了具体的解决方案来实现合规。这样的约束使得相关应用程序的开发变得特别复杂和困难。简化这一过程需要研究新的开发方法，这些方法整合了依赖性概念，并在开发可信应用程序的每个阶段指导开发人员。本文提出了一种设计驱动的方法来指导相关应用程序的开发。这一方法通过一个名为DiaSuite的工具套件实现，并为每个开发阶段提供专门的支持。特别地，设计语言用于描述功能性和非功能性应用。该语言基于专用范例并集成了诸如错误处理之类的依赖性概念。从应用程序的描述中，生成开发支持以指导实施和验证阶段。因此，专用编程框架的生成允许指导实现，而正式模型的生成允许指导静态验证和仿真支持，从而使测试更容易。通过在航空电子学和普适计算领域进行的案例研究对这种方法进行了评估。软件开发、设计语言、代码生成、依赖性我R S M在许多领域，如航空电子、医疗或家庭自动化，软件应用程序发挥着越来越重要的作用，甚至对其环境至关重要为了能够信任这些应用程序，它们的开发受到操作安全要求的约束。事实上，有必要证明，在整个开发周期中考虑了这些高级别要求，并实施了具体的解决方案来满足这些要求。这些限制使得安全操作应用的开发变得特别复杂和困难。促进这一过程需要寻找新的开发方法，这些方法集成了功能安全概念，并指导开发人员完成因此，本文提出了一种以设计为主导的方法来指导安全操作应用的开发。这种方法是通过一套名为DiaSuite的工具实现的，该工具在开发的每个阶段都提供了专用的支持端口。特别地，设计语言允许基于专用范例并通过集成诸如错误处理之类的操作安全概念来描述应用的功能和非功能方面。根据应用程序的描述实际上，专用编程框架的生成允许指导实现，而正式模型的生成允许指导应用的静态验证，通过在航空电子和无处不在的计算领域进行的案例研究对这种方法进行了评估关键词：软件开发、设计语言、代码生成、操作L I T E D S P U B L I C在I O N S本文所讨论的工作已经在前面介绍过了。会议由NC和 S我是一个很好的朋友– 相关应用的设计驱动开发：航空电子学的案例研究– 在普适计算中架构错误处理的域特定方法Wo RksHO PSN与x之比n– 设计驱动的、基于工具的开发方法的实验研究克里斯汀·卢贝里、查尔斯·康塞尔和泽维尔·布兰克邮政服务– 面向传感/计算/控制应用的基于工具的开发方法iii.R E M E R C我是E N TS如果没有许多人的帮助和支持，这篇论文是首先，我要感谢J’ai beaucoup appris à ses我还要感谢Nicolas Loriant的帮助、动力、幽默和建议。和他一起工作是一种真正的乐趣，从我作为博士生的第一步到我的辩护我还要感谢Marc-Olivier Kilijian和Chis-tophe Dony，感谢他们让我也要感谢莫哈-感谢莫斯巴同意主持我的论文评审团。我衷心感谢凤凰队的每一位成员。埃米尔·巴兰，感谢他的许多建议和他使我们的日常生活更愉快和信息丰富的热情。朱利安B.感谢他作为一个经验丰富的博士生的建议，感谢他是一个最令人愉快的同事，无论是在键盘、钢琴、球拍还是啤酒后面。达米安M.我们愉快的交流（甚至月球）。感谢斯蒂芬妮在团队中、在泰雷兹以及作为一名年轻的父母分享了这一冒险感谢本杰明的幽默和建议。朱利安M.感谢他的好意和我们在里诺的冒险，从报纸到赌场。达米恩C. 感谢他的建议和寿司。彭菲为他的好心情万无一失。佐伊的精彩讨论。感谢Christine和Young-Joo的合作和友好。卡米尔，米兰，小查尔斯，保罗和卢克，感谢我们在球队内外的美好时光Hélène感谢她丰富的讨论，这些讨论改变了我们对计算机科学的看法洪，吉斯兰，艾米莉，斯蒂芬，若昂，希尔，尼古拉斯C。感谢你参与团队的工作和良好的氛围感谢Sylvie和Chrystel每天的帮助和善良。我还要感谢ARC SERUS的成员，感谢他们在最后，我要感谢我的母亲、哥哥和姐姐在整个论文过程中给予我的支持我也有一个想法，我的父亲谁传递给我他的热情计算机科学。我最后的感谢是我的两位公主，她们让我的日常生活变得美好，给了我继续前进的动力。V我是你的朋友11号对流1.1论文21.2文件的组织我是你的X52SuRETE从不，不，不。：VOCABU LAIR和 NOCE PTS72.1定义72.2方法83我的意思是，我的意思是，第十一章第十一章3.1实施113.2概念183.3报告24ii APP岩石25岁时4视图ENS EMB L E274.1捐款274.2方法的介绍4.3飞行经理5第33章第一次见面5.1功能描述5.2错误的处理5.3监督436我是你的47号6.1设计驱动的编程6.2支持错误处理497第59章第一次见面7.1静态验证7.2动态验证iii 第67章第一次见面8EVALUATIO N698.1航空业698.2无处不在的计算9工作X ConnE XE S839.1执行情况839.2概念8610 第89章第一次见面BBBlIOGRApHIE93七L I T E D E S F I G U R E SFIGURE1故障、错误、故障8FIGURE2理想的容错元件FIGURE3SCC范式图4DiaSuite30工具化方法FIGURE 5Cap36管理模式规范概述图6DiaSpec38内置异常层次结构概述图7Cap42管理模式错误处理规范概述图8Cap44管理模式的QoS规范概述FIGURE9目标上下文定时自动机-卷61FIGURE10模拟飞行的屏幕截图FIGURE11消防系统功能规范概述FIGURE12消防系统监督层规范概述FIGURE13防入侵系统规范概述FIGURE14信息扩散器规范概述八我是E D E S我是N G S清单1实体分类法摘录34清单2摘自第35清单3交互合同的规范清单4例外规范38清单5应用程序级错误处理规范概述清单6指定列表7QoS约束规范清单8从生成的抽象类Abstract- IntHeading中提取清单9上下文实现的摘录-列表10系统错误报告清单11系统地应用程序级错误处理52列表12延续接口清单13从生成的抽象类Abstract- SensorFailure中提取清单14处理错误的实施义务清单15错误处理实现要求示例清单16传感器上下文实现摘录列表17摘自九I N T R O D U C T I ON1在我们的日常环境中，日志应用占据着越来越重要的位置。在运输、能源、医疗保健、通信或家庭自动化等领域，这种增加的存在不能以牺牲安全运行为代价。实际上，在这样的领域中，软件系统的故障可能严重的健康、环境或经济后果。例如，在航空领域，导航系统的故障可能造成灾难性后果，导致生命损失。在通信中，电话网络的崩溃虽然许多解决方案已经被证明可以保证硬件系统的安全运行，但安全软件的开发面临着两个主要挑战：软件复杂性的增加和安全要求的约束例如，在航空电子领域，关键软件系统必须经过认证，以认证过程要求在软件规范中表达的每一个要求都可以追溯到它在执行代码中的一旦建立了可追溯性，就更容易保证软件的安全运行。然而，建立这种可追溯性是一项更加繁重的任务，因此，开发可靠的软件是一个真正的挑战，即使这些软件承担着越来越多的责任。因此，需要新的方法和工具来促进日志软件开发，并在我们的环境中更好地采用安全软件。12I nTRODUCTIO n1.1他们是E为了应对安全软件日益增长的复杂性，本文提出了一种以设计为导向的事实上，设计驱动的开发方法允许通过在高抽象级别上描述软件来控制软件的复杂性。因此，该描述允许在开发的早期阶段对软件行为进行推理，并指导过程的其余部分。然而，这些方法中的大多数是通用的，因此仅提供有限的安全操作支持。例如，安全要求通常在软件描述中以通用属性的形式表达。这些通用属性可能会在开发过程中被误解，导致为了最好地指导开发，我们的方法依赖于功能安全软件的设计范例。事实上 ， L’approche proposée permet notamment de guider defaçon ri- goureuse安全软件开发的主要限制之一是确保软件规范和执行的代码之间的一致性。事实上，这种保密性是必要的，以确保软件的行为符合规范中规定的要求，并限制意外故障的风险。航空电子软件认证的可追溯性要求是在开发过程中施加的这种约束的一个例子。为了应对这些限制，一套提供开发通过该支持端口允许系统地指导开发，并L’approche因此，我们通过两个领域的发展来说明和验证这种方法：航空航天和无处不在的计算。为了更详细地衡量我们的方法的好处1.2 ORGA nI sATIO nDU文件编号3为了开发安全的操作软件1. 2 ORGA NI S比率 NDU文件NT本文件分为三个部分。首先，我们介绍了最后，我们通过介绍我们的方法在一套工具中的实现、它对各种软件应用程序开发的好处以及实证研究的实现来验证我们的方法第一部分是对这篇论文的科学背景的研究。第2章介绍了在整个过程中使用的功能安全的不同概念，第3章概述了第二部分提出了开发功能安全软件的建议方法。[1]第4章首先对该方法进行了概述然后，第5章、第6章和第7章描述了我们对安全软件开发的设计、实施和验证阶段的建议。本文的第三部分讨论了所提出方法的验证。第8章介绍了主要基于航空和无处不在计算领域的与本论文相关的工作将在第9章中讨论。最后，第10章结束了这篇论文，并讨论了我们工作的未来方向。第一部分C O NT E X T ES R E T D E F O N C T I O N E M E N T：V O C A B U-2L A I R E T T C O N C E P T S本章的目的是这些概念以及用于描述它们的逻辑学借用自Avizienis等人的工作。 [10]和[65]。在定义了安全操作的基本概念之后，我们介绍了用于实现安全操作系统的不同方法。2.1我爱你系统的安全性它可以根据不同但互补的属性来查看，这些属性允许定义以下属性：– 可用性：系统在请求时响应– 可靠性：系统不会因故障而失效– 安全性-无害性：系统– 保密性：系统信息只能由获得授权的人员访问– 完整性：系统不能被外部因素改变。– 可维护性：系统可维修。当所提供的服务偏离其预期用途时，就会发生系统故障当所提供的服务的值不对应于预期结果时，系统可能按值发生故障是一个或多个错误的结果错误是系统的一部分从正确状态到错误状态的偏差当这种偏差到达系统的外部状态时，即当系统提供的服务偏离其预期时，它导致故障。可以检测到错误;否则，将其视为潜在错误。78 SuRETE从不，不，不。： 词汇表和CONCE PT S错误的假定或证明原因故障可以同时具有不同的性质：它是故意的还是偶然的，是系统内部的还是外部的，是在系统开发期间还是在系统运行期间发生的，等等。Avizienis等人提出了不同类型故障的分类。 [10].图1：故障、错误、失败故障、错误和失败的概念是递归的。图1说明了这一现象：系统1的故障可以被认为是包含它的系统22.2方法S为了– 故障预防是指旨在防止故障发生或引入的方法– 容错的目的是防止– L’élimination des fautes permet de réduire le nombre et lasévérité des– 故障预测试图估计故障的数量及其后果。故障预防通常是开发软件系统的过程的一部分。例如，选择强类型语言或严格的programming规则可以限制开发过程中的错误数量。在航空电子领域，DO-178B [33]可以被认为是一个标准，为安全软件系统的开发提供了许多建议。容错是以故障处理为基础的和错误。故障处理的目的是防止处理错误需要设置一个