Lustre
Lustre
复制标题
光泽
DOI：
10.1007/3-540-58867-1_50
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
L. Holenderski
中科院分区：
文献类型：
--
作者：
L. Holenderski
我们的目标是全面开发（即指定、编程和验证）生产单元模拟器的控制器。我们在 Lustre 中指定并编程了控制器，Lustre 是一种用于对同步反应系统进行编程的声明性语言。为了进行验证，我们使用了一个名为 Lesar 的符号模型检查器，它允许自动验证那些仅使用布尔数据的 Lustre 程序。由于生产单元控制器可以编写为这样的程序，因此我们能够自动验证本案例研究的任务描述中给出的所有安全要求。使用声明性语言可以在相对较短的时间内以相对简单的方式开发控制器。
Our aim was to fully develop (i.e. specify, program and verify) a controller for the production cell simulator. We have specified and programmed the controller in Lustre, which is a declarative language for programming synchronous reactive systems. For verification we have used a symbolic model checker, called Lesar, which allows to automatically verify those Lustre programs which use only boolean data. Since the production cell controller could be written as such a program, we were able to automatically verify all safety requirements given in the task description for this case study. Using a declarative language allowed to develop the controller in a relatively easy way, and in a relatively short time.