DO-178B的文章与幻灯片

上次在百度中搜索“王云明”的时候,找到了在网络上流传的二个文件,一个文件是我写的一篇关于DO-178B的文章,另一个是为这篇文章做报告时写的幻灯片,可与文章配套使用。
既然本人的文件已经在网络上流传了,那也应该出现在本人博客里吧。于是我就把这二个文件贴了上来,供会员下载。(还不是会员的赶快注册啊!)
摘要
本文简要介绍了民用航空业界的高安全性嵌入式开发的三个标准:系统生命周期的ARP4754,软件生命周期的DO-178B,以及硬件生命周期的DO254;着重分析了DO-178B 标准所规定的软件生命周期中的开发进程、验证进程、验证的验证进程;针对这些进程在实际工程中实现的困难和挑战,阐述了进程自动化和进程省略的前提条件和相关依据。文章的最后还介绍了SCADE 这一款流行的嵌入式软件开发环境,分析了它如何实现进程的自动化和进程省略并满足DO-178B 标准。SCADE 在国内外的成功应用在文章结尾处也有提及。

关键词:DO-178B,开发进程,验证进程,验证的验证进程,进程的自动化,进程的省略,SCADE
Abstract
This paper briefly introduces three international standards in safety-critical embedded development for civil aircraft: ARP4754 for system lifecycle, DO-178B for software lifecycle, and DO254 for hardware lifecycle; it summarizes the processes described in DO-178B, focusing on the development processes, verification processes and verification of verification processes. After an analysis of the challenges in implementing these processes, this paper describes the premise and the foundation of process automation and process elimination. At the end, this paper introduces SCADE, a popular development environment for embedded software, with detailed information how it attains process automation and process elimination. Some successful applications of SCADE are also mentioned in the paper.
Keywords: DO-178B, development process, verification process, verification of verification process, process automation, process elimination, SCADE
DO-178B嵌入式开发的标准,进程,方法及工具(pdf格式,文章)
DO-178B民用航空嵌入式开发的标准、进程、方法和工具(pdf格式,幻灯片)

47 thoughts on “DO-178B的文章与幻灯片

  1. chenggh说道:

    1,请问目前在D0-178B中,是否包含形式化验证的内容?

    2,请问SCADE对于源代码的验证过程(从设计模型到源代码),只是验证代码stub,这是只是从UML模型生成代码框架,而UML模型则很容易用形式化语言描述 ,还是验证整个源代码?
    如果是整个源代码,请问SCADE采用那种方式?
    目前我所知道的一种方法是,使用Haskell重现整个源代码,就是说使用Haskell把源代码重写一遍,使Haskell代码和C/C++代码具有相同的behaviour,这一步手工。然后使用Hasell-Isabella转换器把Haskell代码转换为形式化语言描述,然后验证,这个过程很是漫长。

    3,请问目前SCADE对于目标代码的验证支持那些平台(从源代码到目标代码)

  2. chenggh说道:

    还有,您如何看待D0-178B和IEC61508这2个标准?

  3. ywang说道:

    引用 chenggh:
    1,请问目前在D0-178B中,是否包含形式化验证的内容?

    很抱歉这么长时间没有给您答复。五一前公司组织春游,五一后放假。到今天才看到您的问题。

    首先,要明确一个概念:“形式化验证”(Formal Verification)是“形式化方法”(Formal Methods)的一部份内容。在DO-178B标准中第12.3.1节简要地提到了“形式化方法”。您可以参阅。

    另外,由于DO-178B标准是面向目标的,它尽可能地不涉及某种具体的开发方法或验证方法。只要您提供足够的证据证明您的机载软件的研制过程达到了相应的目标,就可能通过DO-178B标准的认证。从这个意义上来讲,不使用“形式化方法”开发的机载软件完全也可以通过认证。

    因此,在DO-178B标准中,虽然提到了“形式化方法”,但并不是强制性的要求。它只是一页带过,没有展开很详细的讨论。需要指出的是,在未来的DO-178C标准中,将会有一个专门关于“形式化方法”的Supplement。

  4. ywang说道:

    引用 chenggh:

    2,请问SCADE对于源代码的验证过程(从设计模型到源代码),只是验证代码stub,这是只是从UML模型生成代码框架,而UML模型则很容易用形式化语言描述 ,还是验证整个源代码?
    如果是整个源代码,请问SCADE采用那种方式?
    目前我所知道的一种方法是,使用Haskell重现整个源代码,就是说使用Haskell把源代码重写一遍,使Haskell代码和C/C++代码具有相同的behaviour,这一步手工。然后使用Hasell-Isabella转换器把Haskell代码转换为形式化语言描述,然后验证,这个过程很是漫长。

    您可能对UML工具比较了解而对SCADE了解并不是太多。我先从以下几点回答您的问题,您若需要更深入的了解可以发邮件到consultants_cn@esterel.com.cn并留下您的联系方式,将会有专人与您联系并给你寄去SCADE产品资料或向您介绍和演示。

    第一点:SCADE是“严格的”基于模型的开发,也即绝大部分的软件研制工作都是在模型上进行的:建立模型验证模型并确认模型无误、然后使用模型生成代码和设计文档。而代码生成器KCG通过了DO-178B A级的质量认证,根据标准,生成的代码可以不必再作测试和验证。

    因此,使用SCADE开发工具和开发方法,我们只对模型进行验证(含形式验证),但不需要对SCADE生成的源代码再进行验证。

    第二点:SCADE本身的建模语言就是形式化语言,而不像您所说的“UML模型则很容易用形式化语言描述”……

    第三点:SCADE生成的代码是“产品代码”而不是“框架代码”,也即生成的代码可以不做任何修改(也不做任何验证),就可以集成、编译、使用。相对来说,UML工具生成的常常是“框架代码”,需要在框架内添加自己的手写代码,然后经过验证测试以后才可以编译使用。

  5. ywang说道:

    引用 chenggh:
    3,请问目前SCADE对于目标代码的验证支持那些平台(从源代码到目标代码)

    SCADE生成的代码是机载“应用软件”的代码,它独立于平台,也即SCADE生成的代码可以应用于各个不同的平台。另外,SCADE也提供针对不同平台的接口代码生成,以方便“应用软件”与“系统软件”的集成。详细的平台列表请电邮consultants_cn@esterel.com.cn索取。

  6. tony97说道:

    太好了,谢谢。

  7. chenggh说道:

    王博士您好,可以把DO-178B和DO-254的资料给我一份吗?
    cheng.guanghui (at) gmail.com
    多谢了

  8. Jane说道:

    一个同事发给了我一篇您有关DO-178B国内研究现状的文章,看了之后觉得很有道理就找了你的博客。
    我们有几家供应商用了SCADE工具在机载软件开发过程中。没有记错的话,这个工具是Mike DeWalt进行的A级别C代码生成工具的工具鉴定。

  9. ywang说道:

    引用 Jane:
    一个同事发给了我一篇您有关DO-178B国内研究现状的文章,看了之后觉得很有道理就找了你的博客。
    我们有几家供应商用了SCADE工具在机载软件开发过程中。没有记错的话,这个工具是Mike DeWalt进行的A级别C代码生成工具的工具鉴定。

    先赞一个![face41]
    我自己还不太好意思在这里宣传,你倒帮我宣传起来了,呵呵,谢谢啦!

  10. chenggh说道:

    您发的资料我已经收到,多谢您了。
                                   程广辉

  11. rustic010说道:

    看到您的讲义感觉很简明扼要而且精炼。目前DO178C据说已经完成了意见征求准备发布,另外,去年年底DO160F也已经发布。由于信息闭塞,目前我没有办法获得这方面信息。
    希望您方便的时候可以把DO-160F以及DO-254的中英文版本发给我,感激不尽!
    同时,也希望看到您更多精彩的博文!
    我的邮箱rustic010@yahoo.cn[face01]

  12. zqj_53说道:

    王博士您好,能否将DO-160F以及DO-254的中英文版本发给我,谢谢!zqj_53@163.com

  13. zhangyang1188说道:

    王博士您好,能否发一些DO254方面的文章。我现在在看英文版的DO254,总觉得理解的不太透彻,能否给我发一份中文版的,谢谢!

  14. kcsheu说道:

    王博士您好,可否将DO-160F的中英文版本发给我,谢谢!
    kcsheu@gmail.com

  15. merry1007说道:

    王博士你好  看了一些关于DO-178B的资料,感觉还不是很明白,什么A级的标准有66条,B级65条。。。这些都是什么啊

  16. owesun说道:

    王博士,您好。我也想要一份do-178b和do-254的中文文档谢谢。

  17. ywang说道:

    引用 merry1007:
    王博士你好  看了一些关于DO-178B的资料,感觉还不是很明白,什么A级的标准有66条,B级65条。。。这些都是什么啊

    DO-178B标准最本质的内容,就是针对不同的软件级别(A级、B级、C级……),定义了在机载软件研制过程中需要达到的目标:也即A级软件需要达到66条目标,B级软件需要达到65条目标……

    在定义这些目标的同时,DO-178B标准还针对不同的软件级别,规定了实现这些目标的独立性要求,相应生命周期数据及其控制类别等等。所有这些内容,参见DO-178B的Annex A,表A1到A10。

    在对机载软件做适航认证的时候,质量认证机构的主要任务也就是判断机载软件的研制过程是不是满足这些目标。

    如果还是不解,我们电话交流吧。

  18. ywang说道:

    最近比较忙,二个星期没有上自己的博客,有些问题没有及时解答,有些请求也没有及时答复,请大家谅解。

    现在,多数请求已经通过邮件答复了,感谢大家对我博客的支持。

  19. rainroom说道:

    多谢!
    刚刚开始研究!有什么联系(电话)直接请教?

  20. rainroom说道:

    再打扰下,我也想要一份do-178b和do-254的中文和英文文档。xiedianhuang@tom.com

  21. rainroom说道:

    王总,谢谢!邮件已经收到!
    但由于可能网络问题,不能给你回复邮件!已经和你们销售联系过!
    上海飞机设计研究所

  22. dxing_1983说道:

    有没有arinc615方面的资料啊

  23. daybreak说道:

    多谢王博士!

  24. cdcjl说道:

    王博士您好,我在7月份参加了北京的178B培训,听完收获很多。回来后又上你的博客学习了下。
    另外有个请求:可否将DO-160F的中英文版本发给我,谢谢!
    125875880@qq.com

  25. cbbc123说道:

    王博士你好,正在学习DO-178F,和DO-254,但无中文,可否将DO-160F/DO-254的中英文版本发给我,谢谢!
    CBBC123@126.COM

  26. jiumeiwang说道:

    王博您好,看了你的履历文章博客,实在觉得你肯定是在DO178B方面很资深的人。但是我对于您PDF里面一句话有点疑惑:(SCADE)唯一通过DO-178B A级民航标准质量认证的代码生成器。这个Do178B的质量认证是什么样子的?从来没有听说过,因为它是一标准,怎么会给认证呢?我知道Tool Qualification,你是指这件事吗?如果说通过了这个认证,意味着这个工具生成的代码不用做验证了?还是什么意思?诸多疑问还请王博不赐吝教!

  27. ywang说道:

    引用 jiumeiwang:
    王博您好,看了你的履历文章博客,实在觉得你肯定是在DO178B方面很资深的人。但是我对于您PDF里面一句话有点疑惑:(SCADE)唯一通过DO-178B A级民航标准质量认证的代码生成器。这个Do178B的质量认证是什么样子的?从来没有听说过,因为它是一标准,怎么会给认证呢?我知道Tool Qualification,你是指这件事吗?如果说通过了这个认证,意味着这个工具生成的代码不用做验证了?还是什么意思?诸多疑问还请王博不赐吝教!

    这是好多年以前的文章了,表达的意思没有错,但有些术语的翻译或描述不太符合现在的习惯说法,请谅解。

    当时想表达的其实是您所说的意思,也即SCADE/KCG在多个项目中经过了Tool Qualification,现在行业内常常翻译为“工具的鉴定”。

    根据DO-178B的思想,如果KCG作为一个代码生成器,通过了开发工具的鉴定,那么它生成的代码的验证工作可以省略。这包含了二层意思:

    1、不需要对这些生成的代码进行走查,也即Review,如走查“代码是否符合软件编码标准”等等
    2、也不需要对这些代码进行功能的正确性测试。代码的功能正确性被模型的功能正确性以及KCG的工具鉴定所替代。换句话,KCG的工具鉴定把生成的代码的正确性验证转化成了SCADE模型的正确性验证,这使得验证工作提前实现,帮助我们尽早发现错误。

    希望这样解释能解除您的疑惑。

  28. jiumeiwang说道:

    谢谢您的回复,已经对我的问题很清楚了,但是我还是又发了邮件给您。提了更进一步的问题。

  29. jiumeiwang说道:

    王总,我在你提供的公司网站上还是发现了这句话:
    “SCADE Display?是先进的,面向高安全性显示系统的嵌入式图形设计工具,并通过了军事及航空业的DO-178B标准A级认证。”
    不是我吹毛求疵,是因为您刚给我解释过,我想怎么还在网站首页呢?

  30. ywang说道:

    引用 jiumeiwang:
    王总,我在你提供的公司网站上还是发现了这句话:
    “SCADE Display?是先进的,面向高安全性显示系统的嵌入式图形设计工具,并通过了军事及航空业的DO-178B标准A级认证。”
    不是我吹毛求疵,是因为您刚给我解释过,我想怎么还在网站首页呢?

    呵呵,谢谢您的批评。您的“吹毛求疵”会让我们做得更好。我马上请我们市场部修改网站。

  31. ywang说道:

    引用 jiumeiwang:
    谢谢您的回复,已经对我的问题很清楚了,但是我还是又发了邮件给您。提了更进一步的问题。

    收到您的邮件,给您回复了[face01]

  32. net30说道:

    thanks

  33. nuaa7375说道:

    王总,您好!我也正开始学习Do-178B和Do-254,如果您有中英文的电子版,能不能也给我发一份啊!
    LQH203@nuaa.edu.cn [face01]

  34. lanvid说道:

    王总,您好!我也正学习Do-254,如果您有中文的电子版,
    能不能也给我发一份?
    lanvid@126.com
    谢谢!

  35. bomeya说道:

    王博士您好,能否也发我一个邀请码,不胜感激,谢谢
    bigstarjack@hotmail.com

  36. ywang说道:

    引用 bomeya:
    王博士您好,能否也发我一个邀请码,不胜感激,谢谢
    bigstarjack@hotmail.com

    邀请码已发出,请查收您的邮件。

  37. 菜鸟2008说道:

    王总,能不能发个邀请码给我,我注册不了,拜读了您的一些DO-178B的文章,很有收获,希望能成为会员,和大家交流交流,谢谢!我的邮箱:mywork1980@126.com

  38. njxhm说道:

    王博士,您好!我对DO-178B很感兴趣,能否发给我一个邀请码以获得更多的信息和与大家交流的机会。谢谢!
    njdhm@sina.cn

  39. citybird说道:

    王博士您好,加油站上的讯息不能学习,能否发给我一个加油站邀请码,非常感谢!

    1043849996@qq.com

  40. citybird说道:

    王博士您好,能否也发一份DO-178C标准的资料,以后要从事这方面研究,万分感激您,谢谢!邮箱1043849996@qq.com

  41. echoshy说道:

    王老师,我是6-1-5的,之前上过您的培训课,希望能有更多的学习,希望能成为加油站会员,能否给我个邀请码,谢谢!
    我的邮箱:echoshy@hotmail.com

  42. 灵犀霜翼说道:

    王老师您好,目前正在研究DO系列的最佳实践,看到您的文章,可否给我发个加油站的邀请码,想更多的学习一下,谢谢。
    我的邮箱是baiyu1022@163.com

  43. wyhwah28说道:

    感谢您的分享

  44. 谭伟雄说道:

    王老师,您好!这次有幸在北京参加了您主讲的DO-178B/C培训,受益匪浅,谢谢了。

  45. ywang说道:

    引用 谭伟雄:
    王老师,您好!这次有幸在北京参加了您主讲的DO-178B/C培训,受益匪浅,谢谢了。

    谢谢你的肯定和支持!以后多交流哈……

  46. youzizhile说道:

    王老师,我现在在学习DO-178B标准,遇到一些问题,在网上搜索培训是发现《DO-178B加油站》这个论坛,不知道您能不能给我发一个邀请码,不胜感激,谢谢!我的邮箱是youzizhile@163.com,谢谢

  47. Yunming.WANG说道:

    引用 youzizhile:
    王老师,我现在在学习DO-178B标准,遇到一些问题,在网上搜索培训是发现《DO-178B加油站》这个论坛,不知道您能不能给我发一个邀请码,不胜感激,谢谢!我的邮箱是youzizhile@163.com,谢谢

    邀请码已经发给你了。

发表评论

您的电子邮箱地址不会被公开。 必填项已用*标注