ModelCoder是一款支持多种嵌入式系统建模,并可以生成高安全可靠C代码的软件设计和开发工具。从视频游戏到嵌入核电站的软件,嵌入式软件是电子系统的一部分,通常被设计为具有实时计算的专用功能。在飞机、汽车或者高铁上的关键系统是响应式系统,在该系统中,故障可能导致灾难性的后果。ModelCoder应用于这些有精确标准的关键领域,这些领域的实时系统在运行过程中不停的与其环境进行交互,通过读取数据和事件来产生控制环境的动作。实时的应用程序是一种反应式的程序,他遵循确定性原则。一个系统,如果使用相同的一组输入序列,在相同的时间调度下,其反应情况相同,始终产生相同的一组输出。
ModelCoder采用严格的同步数据流语言,这是确定的声明式的语言。同步原理指出:在执行代码时,输入接收和输出产生之间没有延迟,两次调用之间的输入唯一不变。换句话说,反应时间必须小于两个事件之间的延迟,这意味着每个输出都是在接收下一个输入之前产生的,因此内部处理时间可以认为是空的,周期之间不会产生数据重叠,输出仅由其输入唯一确定,这极大程度上化简了应用程序的设计。
经过近十年的研究,为实现安全关键程序开发环境的国产化目标,迪捷软件研发的ModelCoder工具提供数据流和控制流结构(包括状态机)模型来满足此类程序的开发需求。数据流和状态机已被用于航电、轨道交通以及核工业等众多领域的关键程序开发中。基于模型的ModelCoder工具意味着安全关键领域应用程序的开发方式从原来基于文档的设计转变为基于图形的设计,这种图形的表示基于底层同步数据流语言,不是简单的绘制模型,它是一种过程实践的工具,可以通过仿真验证及早的发现设计缺陷。更重要的是,ModelCoder软件中的代码生成器L2C,采用严谨可信的形式化证明方式,确保输入模型相对于生成的C代码语法语义都正确无误,从而保证模型与代码的一致性。
网友评论