欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
航天嵌入式软件是航天型号任务成败的关键之一．航天嵌入式软件是一种周期性、多模式的软件．软件的每个模式表示系统处于一定的状态，并进行相应的复杂计算．因此，提出了一种名为SPARDL的形式化建模方法．为了满足型号应用的需求，对这一方法进行了若干改进．为了表达航天器的时序性质，提出了一种基于区间逻辑的性质规范语言.为了支持工业应用，还设计了代码生成方法．这一建模方法已在航天工业领域得到了应用．
英文摘要：
The success of aerospace depends on the correctness of aerospace embedded software. Such embedded software are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such software may also involve intensive computing in their modes. Currently, there is lack of domain-specific formal modeling languages for such software in the relevant industry. To address this problem, this article proposes a formal visual modeling approach called SPARDL as a concise and precise way to specify such software. To capture the temporal properties of aerospace embedded software, a property specification language is provided based on interval logic. To support application in industry, code generation methodology is also discussed. This modeling approach is applied in some real-life cases in aerospace industry.
同期刊论文项目
同项目期刊论文
Proving total correctness and generating preconditions for loop programs via symbolic-numeric comput
期刊信息
位置：