1  实时软件开发的规范途径

　　Sildex是一个规范化详细设计和控制/数据功能分析的开发环境,用于复杂和关键性的实时系统设计。使用Sildex,用户可以建模、仿真、正式确认、自动生成优化代码,以生成可执行的详细规格说明,并且在硬件成型之前就生成系统原型。它允许从Simulink和Stateflow中导入数据。

2  应用领域

　　在大多数实时控制或计算要求高的系统中,软件是非常复杂的,这要求采用正式的捕捉和确认工具,例如Sildex。这样才能确保系统正确定义,并且行为符合规格说明书的定义。

　　对于这样的系统,Sildex致力于使开发流程更加顺畅。同一个规格说明的图表,可用于确认规格说明书内部的一致性,可以用于仿真和正式确认系统属性,还可以自动的获得所设计系统的代码。

　　Sildex的应用范围包括控制系统、嵌入式软件、实时系统、信号处理和安全性要求很高的软件（软件失效会导致严重的后果）。这些软件通常出现在航空航天、国防、运输器械、能源和通信等工业领域。

3  既具备数据流也具备控制流的整体环境

　　大多数实时系统由紧密结合的两个方面组成。

　　关注的一个方面是状态转换。一系列计算密集的操作,对应一定输入产生相应的功能输出,并产生进程的内部状态。这些内部状态具有连续性的特征。状态的转换在数量上改变了进程的行为。表达这些行为最方便的手段通常是并行数据流方式。我们举一个计算汽车燃料注入率的例子,这是在驾驶员发出命令产生的功能,见图1。

图1

　　实时系统关注的另一个方面是离散的宏观状态。状态的转换在数量上改变了进程的行为。例如,一个发动机的状态可以是预热、启动或者常速运行,注射率的计算根据发动机当前的状态或系统模式的不同而不同。对这一类型的行为建模,自然使用状态图和控制流的方式。

　　为了兼顾数据和控制两个方面,原来的开发者不得不使用不同的设计流和工具来补充现有工具不完整的功能。当不同的元素集成在一起时,必然因为工具之间设计流的不兼容性导致集成的困难。而且,同时掌握好几个不同的工具和设计方法需要花费更多的时间和经验。

　　Sildex提供了一个完整的环境,允许在系统级别同时说明和分析控制流和数据流。出于相同的考虑,描述PID修正和通信协议时也是如此。通信用图形化的方式通过数据流图来描述,而模式的转换在状态图中进行建模。

4  分层的图形化说明

　　在Sildex图中,每一个元素以图形化的符号来表示其功能。一个元素自身可以由图表示,因此可以分层描述系统,如图2所示。您可以生成一个元素并且将它存储在库中。库中可以增加新的元素,旧的元素可以重用,以节省宝贵的开发时间。

图2

　　为描述每个组件,用户可以选择四种不同的方式：数据流方式、状态机、真值表和Grafcet。用Simulink工具产生的图表可以通过Sildex中的 SimuSild导入。用户还可以用C语言生成组件。然后我们可以用数据流方式把组件用线连接到一起,如图3所示。

图3

5  规范的确认

　　Sildex提供两种确认规范图的高级特性。

　　第一种是集成模拟器(integrated simulator),让用户在将示波器和其它显示设备同图表的输入输出连接好以后,可以交互地执行编译器生成的C代码。在模拟的过程中,您可以亲眼跟踪图表的状态机和数据流的进展过程。通过这种方式,模拟从功能上确认了设计图。

　　另外,用户还可以激活Sildex正式确认器(sildex formal prover)来确认安全性的属性,这些安全性属性常常出现在系统的“非正式规范”中,例如“当安全带未系好时禁止启动”。正式确认的价值在于详尽的模拟。被确认的属性保证100%的正确性,否则,会生成一个反例来突出显示模型中的错误条件。

　　验证机制是自动化的,因此不受在使用交互式验证设备中错误的影响。

6  RTOS库

　　使用Sildex,用户不仅可以对控制和数据之间复杂的交互作用进行建模工作,同时,还可以考虑通过RTOS实现软件多任务。Sildex可以产生一个库,这个库包含许多元素,它们专门用于对并发的系统进行建模,例如预清空动作、共享资源、事件运行和过滤、FIFO缓冲器等。

7  模型设计

　　当规范被确认以后,用户可以对模型进行注释,从而根据设计的合约和标准（例如可测试性标准）将系统分成更小的模块。

8  嵌入式代码生成

　　Sildex的编译器可以针对最终系统生成C、Ada和Java代码。这个过程紧凑、迅速,而且不需要调用特殊的库。生成的代码结构是可靠的,因为编译器已经对各种可能出现的方面和规范的必然结果进行了检查。

　　生成的代码可依据规范进行跟踪,而且独立的编译产生模块代码。

9  保证一致性

　　模拟、属性验证和代码生成都依靠一种完整、严格、数学定义的符号体系：同步语言SIGNAL。它是由INRIA(Institut National de Recherche en Informatique et Automatique, Rennes, France)发明的。

　　此语言在Sildex中的使用隐藏了应用中纯软件的方面。因此阅读Sildex规范并不需要掌握SIGNAL语言。

10  好处

　　使用Sildex,系统的设计者可以：

　　◆ 实现开发进程的流水作业,从说明书到执行到测试,都可以减少翻译和沟通的成本;
　　◆ 详细说明非常复杂的实时系统,包括数据、控制和模块、环境内的多任务RTOS的交互作用;
　　◆ 在开发进程的前期,检测详细说明书的错误和二义性;
　　◆ 对关键和安全的方面进行正式确认;
　　◆ 在模型的集成测试确认中,开发的测试脚本可以重用;
　　◆ 自动生成优化的软件代码;
　　◆ 可对应用特有的库和RTOS库进行重用,加速开发进程。

　　Sildex是将来ModelBuild最主要的技术基础,ModelBuild是欧洲IST“Safe Air”项目（请见www.safeair.org）。ModelBuild用于关键实时系统的虚拟集成。

11  主要特点

(1)  Simulink设计输入

　　◆ 自动的Simulink和Stateflow离散时间设计的输入。
　　◆ 保留Simulink图形化方面。
　　◆ 输入数据总线,向量/矩阵操作,转入/转出。
　　◆ 通过数据图形进行自动类型推断。
　　◆ 极快速的输入设计仿真。
　　◆ 通过输入设计产生非常紧凑的代码。
　　◆ 可对输入设计进行模型检测。

(2)  定点代码产生

　　◆ 生成C 和 Ada代码。
　　◆ 从单个的规范（specification）可以产生浮点或定点的代码。
　　◆ 专业领域及其表示的格式化描述。
　　◆ 自动通过数据流图形和最优化格式实现的领域推断。
　　◆ 自动通过计算实现最小损失解决方案。
　　◆ 定点兼容的交互式仿真。

(3)  生成Spark Ada

　　自动注释产生。

(4)  增强型的模块编辑器

(5)  DC +输入/输出（SACRES方法）

(6)  可跟踪的需求

(7)  自动生成文档

(8)  支持的平台

　　PC: Windows 95/NT和SUN: Sparc Solaris。