博士论文EUNIVERSITERANCHE-COMTN结合SysML和SystemC模拟和验证复杂系统提交人的论文阿巴斯·阿卜杜拉泽兹·阿卜杜拉米德并提交给弗朗什-孔泰大学部分满足获得学位的要求哲学博士专业：信息学于2016年3月4日在陪审团面前公开辩护，陪审团由以下人员组成：埃马纽埃尔·格罗洛报告员教授，丽莎， ISAE-ENSMA，文森特·波里兹报告员大学教授，普瓦捷拉米亚，大学巴伦西亚人MamounFilali胺审查员导演从研究CNRS、IRIT、哈桑·蒙塔西尔论文主任图卢兹大学大学DISC/Femto-ST教授艾哈迈德·哈马德论文的共同导师弗朗什-孔泰MDC、DISC/Femto-ST、大学布鲁诺·塔蒂布埃论文的共同导师弗朗什-孔泰MDC、DISC/Femto-ST、大学弗朗什-孔泰X X X确认文件在这里，我想感谢每一个人，谁的帮助和参与，使这篇论文可能。首先，我想对我的论文导师表示最深切的感谢和尊敬。哈桑·蒙塔西尔和我的共同主管艾哈迈德·哈马德和布鲁诺·塔蒂布埃博士。我无法表达我的感激之情。他们的技能，他们的科学僵化，和他们的洞察力给了我很多。尽管如此，我还是感谢他们的组织，感谢他们四年来为我提供的专家建议，感谢他们温暖的人性，特别是感谢他们给予我的信任。我永远不想更自豪地感谢叶海亚法雷斯美狄亚大学教授Messaoud Rahim教授，感谢他的顾问和科学专家帮助和指导我完成了这篇论文。我衷心感谢以法国校区、穆斯坦西里耶大学和F. anche- C. om t e大学为代表的伊拉克高等教育和科学研究部在开展本论文方面的合作。我感谢VESONTIO的工作人员，感谢他们支持我工作的友好因此，我要感谢奥斯卡·卡里略、让-玛丽·戈蒂埃、皮埃尔-西里尔·希姆、哈米达·布阿齐兹、哈娜·我向DISC的工作人员表示感谢，感谢他们在友好和温暖的气氛中支持我的工作。因此，感谢奥尔加Kouchnarenko，主任的DISC（复杂系统信息学）部门在贝桑松，做- minique Menetrier，让米歇尔Caricand，洛朗Steck和所有其他人，如果我忘记了他的名字。感谢他们不懈的支持和鼓励。最后，我要感谢我亲爱的朋友，包括Bassam Alkindy、Huda Al-nayyef、Bashar Al-Nauimi、Lemia Louail，他们分享了我的希望和研究，他们在困难时刻给了我安慰，我与他们分享了难忘的时刻。七奉献献给我的妻子Yusra，用我的爱，它给了我力量去度过我学习中最艰难的时刻。我还要向我的父母、姐妹和她们的家人、兄弟和她们的家人，以及我可爱的家人，表达最强烈的感谢，感谢他们在我多年的研究中对我的论文的支持和鼓励。他们的爱和信任每天都指引着我。谢谢你，妈妈，爸爸，让我成为今天的我。九首字母缩略词BDD块定义图。EMF Eclipse建模框架。MBSE基于模型的系统工程IBD内部块图。INCOSE 国际系统工程理事会OMG对象管理组PD参数图。研发需求图。SCV SystemC验证标准。SCNSL SystemC网络模拟库。SE系统工程。SMD状态机图。SPIN简单Promela解释器。SysML系统建模语言。UML统一建模语言。十一内容物I背景、动机及相关作品11简介31.1动机。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...41.2问题描述。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...51.3论文目标。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...61.4捐款。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ...61.5出版物。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...91.6论文大纲。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...92相关作品112.1引言。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ...112.2复杂系统的建模。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...112.2.1半正式语言。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...122.2.2正式语言。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...122.2.3硬件描述语言。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...132.3 SysML设计的验证。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...142.3.1SysML设计的 验证 。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...152.4 SystemC设计的验证。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...172.4.1使用SystemC环境。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...172.4.2转换为模型检查和工具。... ... ... ... ... ... ... ... ... ... ... ... ...202.5总结。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...21二 科学背景233相关概念253.1模型验证和确认。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...253.2系统工程和MBSE。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...273.2.1SysML。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...... ... ... ... ... ...273.2.2 SysML环境... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...28十三xiv内容3.2.3SysML架构283.2.4使用SysML31的优势3.3使用SystemC31进行仿真和验证3.3.1SystemC语言体系结构323.3.2SystemC仿真环境363.4通过模型检查进行验证373.4.1时间逻辑383.4.2Promela383.4.3模型检查器工具393.5模型驱动工程413.5.1Eclipse建模框架413.5.2使用ATL41进行模型转换3.5.3使用Acceleo43进行代码生成3.6结论434悲剧性轻度病例研究454.1导言454.2功能性和非功能性要求454.3需求分析464.4SysML案例研究模型474.5结论55III捐款575使用SystemC59模拟SysML规范5.1导言595.2从SysML到SystemC605.2.1模型/元模型变换605.2.2SysML Meta-Model615.2.3SystemC元模型625.2.4模型转换技术625.2.5将SysML转换为SystemC645.2.6转换规则645.2.7SystemC模型到SystemC代码65的转换5.3通过模拟进行验证66内容xv5.3.1SystemC仿真675.3.2SystemC网络仿真库685.3.3第68代的痕迹5.4案例研究69的实验5.4.1将SysML与SystemC695.4.2模拟695.5结论726SystemC型号75的验证技术比较6.1导言756.2SystemC验证技术756.2.1SystemC库验证766.2.2与SystemC78集成的库验证6.2.3通过模型检查工具进行验证796.3UPPAAL和TTTL796.4用于UPPAAL验证的SystemC模型的转换816.5案例研究82中的插图6.6SystemC83中的验证分类6.7结论857SysML规范向Promela-SPIN87的转换7.1导言877.2接近877.3从SysML到Promela897.3.1Promela MetaModel897.3.2转换过程897.3.3SysML到Promela转换917.3.4映射转换规则917.3.5Promela Model937.3.6将Promela型号转换为Promela代码947.4使用SPIN工具94进行验证7.4.1LTL型号检查957.4.2验证957.5案例研究95中的插图7.5.1将SysML与Promela967.5.2功能要求97十六、内容7.5.3LTL属性的验证987.6结论98IV结论和未来工作1018结论和观点1038.1主要贡献1038.2未来工作105我背景、动机及相关作品11简介内容物1.1动机41.2问题描述51.3论文目标61.4捐款61.5出版物91.6论文大纲9如今，模型在设计复杂工业系统中的使用不断增加。这些模型通过分析可能的故障和风险，帮助验证早期应用程序的正确性。系统工程（SE）[Blanchard等人，1990]，是一个跨学科的领域，作为管理发展复杂性的明智方法而出现。该模型最突出的特点是将精确的可视化建模系统和最佳实践应用于SE活动。在整个系统开发生命周期（SDLC）中，SE活动包括需求分析、验证、功能分析、分配、性能分析和系统体系结构规范。基于模型的系统工程（英语：Model-Based Systems Engineering，缩写为MBSE）是一种使用计算机模型设计系统的方法。 MBSE专注于在开发周期的早期确定客户需求和所需的功能。模型规范在考虑整个问题（包括功能和非功能要求、验证、测试和成本）的同时，进行设计综合和系统验证在过去的几十年里，MBSE在关键和复杂系统的分析和综合中系统建模语言（SysML）[OMG，2012]由国际系统工程委员会（INCOSE）1提出，并由对象管理组（OMG）标准化。SysML是一种图形建模语言，它允许对复杂系统进行建模以指定和设计它模拟了这样的系统的软件方面以及它们的硬件方面。SysML非常适合在早期的符号阶段描述系统，这是由于它的简单性和图形表示法。然而，SysML是一种半形式化语言，它缺乏支持验证和确认技术的形式语义。在基于模型的开发过程中，验证和确认技术被用来更好地理解模型并评估模型中隐含的模型属性验证和确认过程支持正确的标本-1小时http：www.incose.org/34第1章. 引言模型和探索其他建模替代方案。但是，缺少在验证和确认过程中使用SysML的规范。在已经存在并已标准化的系统的验证和确认阶段中使用的许多技术和方法，从形式验证、模拟和/或测试技术[Kleijnen，1995]，[Debbabiet al.， 2010年]。SystemC[Aynsley，2006]是一种基于C++的开源系统级设计语言，它有自己的仿真内核。通过将SysML与SystemC相结合，我们利用SysML来描述复杂系统，并利用SystemC环境提供的仿真功能这可以通过将SysML图转换为SystemC模型来实现。模拟是用于分析复杂系统规格的常规技术[Kelton等人，2000年]。基于仿真的方法确保初始数量的用户指定的系统路径满足期望的规范。就执行时间而言，它几乎是廉价的，但它只验证了特定计算路径的系统行为。为此，模拟是一种允许验证系统的一些特定执行跟踪的技术。模型检查[Clarke等人，[1999]是一种自动化技术，它给出了一个系统和形式属性的初始状态模型，系统地检查该属性在该模型中的位置。提供一种使用基于模型的技术对SysML规范进行正式验证的方法，非常适合确保所设计系统的有效性，从根本上说是考虑其行为要求。在本文中，我们提出了使用仿真和验证技术验证SysML规范的综合贡献本章组织如下，第1.1节介绍了组织的血液激发。然后，第1.2节描述了问题陈述。第1.3节列出了本文的目标。稍后，第1.4节和第1.5节对所提出的方法进行了概述，并描述了本论文的主要贡献。最后，第1.6节介绍了论文概述。1.1/动机复杂和关键系统的正确设计对工程师来说仍然是一个挑战。在早期设计阶段未检测到的设计中的错误可能会非常昂贵。因此，复杂和关键系统的开发需要验证和确认技术来实现系统模型的检测和校正对于每个建模阶段，我们都需要确保系统的实施符合初始要求。形式化方法是用于将复杂系统建模为数学对象的技术。建立复杂系统的精确数学模型，以比实际测试更精确的方式验证系统属性是可行的[Bode Voix等人，2005年]。我们的目标是将形式化方法与工程应用相结合，这样所有的开发、推理和分析都是形式化方法的应用。形式技术可以应用于设计验证模型，但没有明确的原因。因此，形式化方法必须专门适用于信息系统的发展。建议使用验证技术来验证和确认系统设计。1.2. 问题描述5然而，形式化描述可能难以构建、阅读和理解，尤其是对于非专家。SysML是一种半形式化语言，它似乎是一种固有的折衷，特别是当我们为以后设计的系统提供验证和确认方法在本文中，我们使用SysML、SystemC和模型检查技术。SysML以高抽象级别描述的目标系统。SystemC环境通过模拟验证属性。和模型检查以使用正式的meth-ods验证系统属性。SysML是一种建模语言，用于获得复杂系统的规范，包括需求、结构和行为部分。SystemC语言是传统语言的首选替代语言，其模拟内核是设计用于通过模拟评估系统行为的重要方面模型检查技术允许通过确保满足系统的每个可能状态来验证形式模型上的属性。因此，它与转换函数要求相结合，用于验证和确认SysML模型指定的复杂系统。事实上，关键应用程序的日益重要性刺激了对将SysML与模型检查工具相结合的建模技术的研究，例如SPIN（Simple Promela Interpreter）[Holzmann，1997]和UPPAAL [Larsenet al.， 1997年]。1.2/问题描述为了设计复杂的系统，我们需要一种由高级语言支持的方法来指定和建模系统的不同方面，包括需求、结构和行为。SysML是一个用于指定和建模复杂系统的UML模板，以及用于提供系统设计验证和确认的形式化自身。结合SysML的验证和确认，复杂系统开发的设计阶段是本文SysML规范的验证和确认需要采用成熟的验证技术，如正式验证和模拟。论文问题的解决方案是将仿真和验证通信方法与SysML相结合。• 如何使用SysML模型识别、半形式化和结构化非正式复杂系统需求？• SysML如何与SystemC结合以验证复杂系统的非功能需求• SysML如何与模型检查相结合以提供系统功能需求的正式验证6第1章. 引言1.3/论文目标本工作旨在支持MBSE范式在基于模型的设计子领域的应用，以及基于模型的验证和确认。它将SysML规范与SystemC相结合，以模拟建模行为。此外，SysML与模型检查方法相结合，以应用形式验证和确认技术。本工作中开发的策略允许从半正式规范（如SysML）创建系统设计模型，这些模型在正式我们使用形式验证来检查复杂系统模型的要求。验证和确认过程通过模拟非功能特性和正式验证来完成，以确保满足功能要求。基于本论文中可用的各种定义，我们描述了设计和创建一个可以模拟和正式验证的系统模型规范的过程在特定条件下，我们可以评估相应的真实系统的行为。在本文中，我们描述了与规范和验证方法相关的一系列活动，用于评估复杂系统设计的正确性。SysML带来的改进使其在工业和学术环境中的受欢迎程度系统的SysML规范由需求图、描述系统的动态操作的行为图（如状态机图（SMD））和描述静态模式下的系统的结构图表示。后来，块由三个图建模：块定义图（BDD），其表示块的体系结构及其执行的操作，以及内部块图（IBD）和参数图（PD），其用于表示每个块的端口以及它们之间链接它们的端口的连接器系统设计是SysML中的一个重要概念虽然它基于一种可以从抽象级别开始的开发方法，但它可以在从SystemC环境到模拟或从模型检查到验证的实现中结束。1.4/贡献在本文中，我们提出了旨在设计、验证和验证复杂系统的贡献。这些贡献有助于应对上一节提出的挑战。在图1.1中，我们展示了我们对SysML规范、SystemC环境和模型检查的贡献（编号为1、2、3和4）第一个是通过分析需求来定义基于SysML的方法，它确定了这种语言必须支持的概念和使用类型。此类要求由要求和规范模型解决。我们创建了问题域的形式化模型，该模型描述了发现问题的环境的行为和结构特征。首先，我们必须创建SysML图来指定系统结构、需求和行为。然后，SysML图被映射到SystemC模块。我们使用SystemC代码运行模拟，以获得行为的跟踪。
我的内容管理
展开
