Using a Process Algebra to Control B Operations
Using a Process Algebra to Control B Operations
复制标题
使用过程代数控制 B 操作
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Steve A. Schneider
中科院分区：
文献类型：
--
作者：
H. Treharne;Steve A. Schneider
B-Method是一种基于状态的形式化方法，它根据在操作下状态变化的机器来描述系统行为。进程代数CSP是一种基于事件的形式化方法，支持对系统行为模式的描述。本文讨论了这些互补视图的组合，其中使用CSP来描述B抽象系统的控制执行。我们将讨论两种观点之间的一致性，以及如何正式确立这种一致性。一个典型的航空电子系统激励工作。本文介绍了该系统的规格和控制实现。并讨论了与其他方法的关系。
The B-Method is a state-based formal method that describes system behaviour in terms of MACHINES whose state changes under OPERATIONS. The process algebra CSP is an event-based formalism that enables descriptions of patterns of system behaviour. This paper is concerned with the combination of these complementary views, in which CSP is used to describe the control executive for a B Abstract System. We discuss consistency between the two views and how it can be formally established. A typical avionics system motivates the work. Its specification and control executive are presented in the paper. The relationship with other approaches is also discussed.