使用同步数据流语言LUSTRE进行实时系统编程与验证
需积分: 10 50 浏览量
更新于2024-09-09
收藏 946KB PDF 举报
"Synchronous Data-Flow Language LUSTRE - 使用LUSTRE同步数据流语言编程和验证实时系统"
本文探讨了使用同步数据流语言LUSTRE进行关键实时系统设计和验证的优势。LUSTRE是一种异步数据流语言，它与关联的验证工具LESAR结合，能够有效地用于程序设计、关键属性的规范以及这些属性的验证。
一、语言介绍
LUSTRE语言由Nicolas Halbwachs, Fabienne Lagnier和Christophe Ratel等人开发，其设计目标是提高编程效率，特别是针对传统实时系统领域中广泛使用的描述工具。LUSTRE的特点在于它支持同步编程模型，这使得数据流在系统中的处理方式更加清晰和直观。
二、编程与验证
通过LUSTRE，开发者可以以一种结构化的方式定义系统的数据流行为，同时利用LESAR进行形式化的设计和验证。论文通过一个简单的示例，演示了如何使用这两种工具来构建一个程序，定义其关键属性，并确保这些属性在执行过程中得到满足。这展示了LUSTRE在处理实时系统时的灵活性和强健性。
三、形式化验证的重要性
文章强调了程序验证的关键角色，尤其是在安全性和可靠性至关重要的实时系统中。LUSTRE提供的形式化方法能够帮助检测和预防潜在的错误，从而减少系统在实际运行时可能遇到的问题。
四、相关研究与应用
LUSTRE及其应用已经在多篇论文中有所介绍，但本论文的重点更偏向于程序验证。作者们提供了一个初步版本的论文概述，进一步阐述了在LUSTRE中进行模型检查和反应式系统验证的方法。
五、关键词
数据流语言、形式化验证、模型检查、反应式系统、同步编程
LUSTRE作为一种同步数据流语言，不仅简化了实时系统的编程过程，还增强了验证能力，确保了系统关键特性的正确性。通过LESAR工具，开发者可以更加自信地设计和分析复杂的实时系统，降低了由于潜在错误导致的风险。
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING,
VOL.
18,
NO.
9,
SEPTEMBER
1092
785
Programming and Verifying Real-Time
Systems by Means
of
the Synchronous
Data-Flow Language LUSTRE
Nicolas Halbwachs, Fabienne Lagnier, and Christophe Ratel
Abstruct-
We investigate the benefits of using a synchronous
data-flow language for programming critical real-time systems.
These benefits concern ergonomy-since the dataflow approach
meets traditional description tools used in this domain-and
ability to support formal design and verification methods. We
show, on a simple example, how the language LUSTRE, and
its associated verification tool LESAR, can be used to design a
program, to specify its critical properties, and to verify these
properties.
As
the language LUSTRE and its uses have already been
published in several papers (e.g.,
[U],
[IS]),
we put particular
emphasis on program verification.
A
preliminary version of this
paper has been published in
[28].
Index Terms-Data-flow languages, formal verification, model
checking, reactive systems, synchronous programming.
I.
INTRODUCTION
T
IS
useless
to
repeat why real-time programs are among
I
those in which errors can have the most dramatic con-
sequences. Thus these programs constitute a domain where
there is a special need for rigorous design methods. We
advocate a “language approach”
to
this problem, arguing
that
the programming language used has a direct influence in the
quality of the software, from several points of view.
1.
The language should allow a natural description of the
problem
to
be solved. In particular, it should be close
to
the traditional tools used in its application field.
2.
The language should be formally sound, in order
to
support formal verification methods.
3.
The language should be simple enough
to
minimize the
risk of misunderstanding about program meanings.
These were our main goals in designing the language
LUSTRE
[Ill, [18]. To meet criterion
1),
we started from the traditional
differential equations, finite difference equations, and boolean
equations can be straightforwardly translated, respectively,
into analog schema, block-diagrams, and gate networks. At
least the class of high level tools also meets our criterion
2),
since they are derived from the mathematical language.
Other authors (e.g.,
[2],
[23])
claimed that such declarative
formalisms are simpler and cleaner than usual imperative
languages, where assignments, side-effects, aliasing, and pa-
rameter passing mechanisms, are unnatural phenomena which
are difficult
to
understand and manage. We agree with this
claim, and therefore consider that these declarative formalisms
constitute a good basis for designing a programming language
meeting the criterion
3).
Lustre is a synchronous data-flow language, initially in-
spired from
LUCID.
As
in
LUCID,
any
LUSTRE
variable or
expression is considered
to
represent the sequence of values
it takes during the whole execution of the program, and
LUSTRE
operators are considered
to
operate globally over these
sequences. The synchronous nature of the language consists in
assuming that all the variables and expressions in a program
take the n-th value of their respective sequences
at the same
time.
More concretely, a program is intended
to
have a cyclic
behavior, an execution cycle consisting in computing the n-th
value of each variable or expression. Basically, a program is a
set
of equations. When we write an equation “X=E,” where
X
is
a variable and
E
is an expression, we mean that the sequences
of values associated with
X
and E are identical (it is an actual
equation, in the mathematical sense), or equivalently, that at
any cycle of the program,
X
and
E
take the same value.
Time and Svnchronv
description tools used in the design of process control sys-
tems.
At
a higher level, these tools consist of mathematical
formalisms (differential equations, boolean equations, etc.),
while at a lower level, people often use data-flow nets (block-
diagrams, analog schemas, switch or gate networks, etc.).
These two classes of tools are closely related: for instance,
The “real time” capabilities of the language are derived
from this synchronous interpretation, like in other synchronous
languages [6],
[8],
[13],
[21],
[24].
We consider the following
logical notion of time: As soon as we can specify the order
or simultaneity relations between events occurring both inside
and outside the program, we can express time constraints about
~~
the behavior of the program. For instance, a constraint like
--
Manuscript received November
1,
1991; revised June 2, 1992. This work
was partially supported by ESPRIT Basic Research Action
SPEC
and by
a
contract from Merlin Gerin. Recommended by R. Kemmerer and C. Ghezzi.
~~any
Occurrence
of
a
dangerous situation must be followed
by
the
emissiorz
‘fan
within
Of2
seconds”
N. Halbwachs and
F.
Lagnier are with LGIIIMAG, 38041 Grenoble Cedex,
will be expressed as
France.
France.
“after any occurrence
of
the event
dangeroussituation
there
must be an occurrence
of
the event alarm before the
2nd
next
C. Ratel is with Merlin-GerinISES and IMAFILGI, 38041, Grenoble Cedex,
IEEE
Log
Number 9202409.
occurrence
of
the event
second.”
0162-8828/92$03.00
0
1992 IEEE
下载后可阅读完整内容，剩余8页未读，立即下载
2022-01-11 上传
2022-09-24 上传
2011-11-25 上传
2023-05-16 上传
2023-07-29 上传
2023-06-06 上传
2023-06-04 上传
2023-06-04 上传
2023-05-30 上传
丽娃河畔
- 粉丝: 19
- 资源: 3
我的内容管理
展开
最新资源
- WPF渲染层字符绘制原理探究及源代码解析
- 海康精简版监控软件：iVMS4200Lite版发布
- 自动化脚本在lspci-TV的应用介绍
- Chrome 81版本稳定版及匹配的chromedriver下载
- 深入解析Python推荐引擎与自然语言处理
- MATLAB数学建模算法程序包及案例数据
- Springboot人力资源管理系统：设计与功能
- STM32F4系列微控制器开发全面参考指南
- Python实现人脸识别的机器学习流程
- 基于STM32F103C8T6的HLW8032电量采集与解析方案
- Node.js高效MySQL驱动程序：mysqljs/mysql特性和配置
- 基于Python和大数据技术的电影推荐系统设计与实现
- 为ripro主题添加Live2D看板娘的后端资源教程
- 2022版PowerToys Everything插件升级，稳定运行无报错
- Map简易斗地主游戏实现方法介绍
- SJTU ICS Lab6 实验报告解析
