Integrated architectural modeling and analysis for high-assurance command and control system design

A Real-Time Architectural Specification (RAS) approach and its application to command and control (C2) systems are presented. Our objective is to establish a formal foundation that will enable us to integrate existing rich but fragmented formal techniques for system specification and verification into a practical and scaleable formal engineering method to support the design and development of highly reliable real-time distributed systems. The contribution of RAS is twofold: First, it provides a formal system that integrates system's timing requirements and requirements propagation into the process of architectural modeling and design in such a way that allows us to systematically enforce that the requirements are met in every step of the design process. Second, it offers an incremental and more scaleable approach for design modeling. These two features together make RAS a suitable model for the design of C2 systems. We further present an incremental method for verifying timing properties of an RAS model that helps to reduce the complexity of analysis both at a given design level and across different design levels. This revised version was published online in June 2006 with corrections to the Cover Date.     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

一种嵌入式实时系统软件的形式化开发方法

领域特征突出的嵌入式实时系统软件开发,既需要严格地保证可靠性又要充分反映实时和交互行为特征,针对这种需要,该文提出了一种从需求分析到体系结构建模直至使用组件技术实现软件的形式化开发方法。文章在介绍了目前的各软件工程领域以及各软件开发阶段中的形式化模型和工具的现状和特点后,引入需求分析的模型和体系结构建模的描述语言,分析其长处和不足,最后对该方法与移动组件结合的前景进行了展望。     

Rule-based systems formalized within a software architectural style

This article considers the utilization of architectural styles in the formal design of knowledge-based systems. The formal model of a style is an approach to systems modeling that allows software developers to understand and prove properties about the system design in terms of its components, connectors, configurations, and constraints. This allows commonality of design to be easily understood and captured, leading to a better understanding of the role that an architectural abstraction would have in another complex system, embedded context, or system integration. In this article, a formal rule-based architectural style is presented in detail using the Z notation. The benefits of depicting the rule-based system as an architectural style include reusability, understandability, and the allowance for formal software analysis and integration techniques. The ability to define the rule-based architectural style in this way, illustrates the power, clarity, and flexibility of this specification form over traditional formal specification approaches. In addition, it extends current verification approaches for knowledge-based systems beyond the knowledge base only.     

基于对象的分布式实时系统调度模型研究

为了解决分布式实时系统有关分配和调度等问题，给出并用形式化方法描述了一种基于对象分布式实时系统调度的通用模型。该模型包括表示时限的绝对时间约束，表示周期属性的周期约束，表示各种前趋关系和同步要求的相对时间约束以及保证资源使用一致性的一致性约束，此外该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时的约束的不足，允许从方法和活动上描述所需的约束，降低了单一约束描述的繁杂程度，为了能够使用现有调度算法进行任务调度，讨论了约束转换的问题，给出了高层约束到底层约束的转换规则和相应的转换算法。     

一个面向对象的二级并发模型

本文提出了一个面向对象的二级并发模型ＦＯＲＣＥ－Ｍｏｄｅｌ．它从需求规范的角度充分开发对象间和对象内两个层次上的并行性，从而将面向对象与并发性有机地结合起来，提供了有效的实时系统建模框架．基于该模型，我们开发了一个多视点可视规范语言族ＦＯＲＣＥ－Ｌａｎｇｕａｇｅ．     

ASADAL/SIM: an incremental multi-level simulation and analysis tool for real-time software specifications

Despite considerable advancement in software engineering methods during the past three decades, requirements engineering of large and complex software systems still remains a difficult and active research problem. One such difficulty lies in developing correct and useful methods for the validation and verification of real-time software specifications. One way of analyzing and validating/verifying software specifications is to mathematically derive or prove desired system properties based on formal specification languages. A full scale system analysis using such formal methods is limited in practice because of the required mathematical skills and computational costs. Formal methods are often used to check only a few very critical real-time properties. Simulation is a complementary approach to testing various system characteristics and validating user requirements. It is especially good for providing a rough picture of final system behavior. This paper presents ASADAL/SIM, a tool for multi-level simulation and analysis of real-time software specifications. It is a subsystem of a larger computer-aided real-time software development environment called ASADAL, and complements ASADAL/PROVER, another subsystem of ASADAL which is a formal verification module.^1. With ASADAL/SIM, simulation primitives can be added to evolving specifications in order to assign stochastic behaviors to external entities and internal processes, and to build a simulation model. ASADAL/SIM can execute the model and, at the same time, demonstrate the final system behavior by graphically showing internal workings of the system; catch undesirable system behaviors with breakpoints; and present various analytical results and system statistics ASADAL/SIM, following ASADAL's philosophies of hierarchical system modeling and early system validation, allows users to simulate ‘evolving’ specifications at different, mixed, and wide levels of detail. In particular, algorithmic details may be specified for low level behavioral blocks, and simulated with abstract entities yet to be refined to such a level. This facilitates the tracking of critical data values at the specification level, and eases the next transformation into code level implementation. With ASADAL/SIM, ASADAL becomes an effective and comprehensive supporting tool for various existing software engineering approaches, particularly top-down refinement and incremental development practices. © 1998 John Wiley & Sons, Ltd.     

Telecommunications service development: A design methodology and its intelligent support

This paper describes a development life cycle for telecommunications services, emphasizing requirements capture, formal specification and validation. The service is developed along the three dimensions of the methodology: refinement, completeness and formality, aiming for a complete, consistent and formally specified service definition. The described methodology can be integrated into currently existing development life cycles which employ formal methods for service creation. Active support for the proposed life cycle is provided by a novel expert system called Requirements Assistant for Telecommunications Services (RATS), currently under development. It actively helps during requirements acquisition and early analysis, and encourages specification reuse with the help of a semi-automated negotiation process. The RATS tool advises the service developer during all stages of the service development, and on different levels of abstraction, and provides requirements management facilities, like traceability, impact analysis and document generation. Some of the features are illustrated using examples from the Universal Personal Telecommunication (UPT) service.     

一种面向嵌入式实时软件的需求建模语言

针对嵌入式实时系统复杂动态交互行为和严格实时的领域特征,提出了一种软件需求规约语言RTRSM。该语言以扩充的层次并发有穷状态机HCA为核心,以支持合成的模板为基本组成单元．利用转换有效期和事件预定机制来描述时间限制,既具有较强的时间限制描述能力,又能自然而直接地支持交互行为的建模,可执行且具有良好的形式语义。给出了该语言的形式化语法,举例说明了其时间描述机制,并通过执行步算法和基于HCA项的结构化操作规则定义了该语言的形式化操作语义。     

Specifying transaction-based information systems with regularexpressions

The work is about the formal specification of transaction-based, interactive information systems. A transaction is a task that the user can execute independently, and the system can be defined as a partially ordered set of transactions. The general framework is the transformational paradigm, based on the classical Waterfall development model (W.W. Royce, 1970). The stages are systems analysis, software specification, design, and implementation. The systems analysis and software specification stages are covered. An informal, transaction-oriented method for systems analysis is proposed. The resulting system specification involves two parts: a high-level specification of each transaction and a formal specification of the system's control flow, i.e., the order of execution of the transactions. The system's control flow is expressed in a formal language describing concurrent regular expressions built on transaction names. At the software specification stage, some operational requirements, such as connect/disconnect transactions and the application of the all-or-nothing principle, are added to the system specification. Then a serial product automaton (SPA) is used to transform the concurrent expression into a single regular expression. This result is proven to be consistent with the system specification     

Methods for the Development of Distributed Real-Time Embedded Systems Using VDM

The development of distributed real-time embedded systems presents a signi-ffcant practical challenge both because of the complexity of distributed computation and because of the need to rapidly assess a wide variety of design alternatives in early stages when requirements are often volatile. Formal methods can address some of these challenges but are often thought to require greater initial investment and longer development cycles than is desirable for the development of noncritical systems in highly competitive markets.In this paper we propose an approach that takes advantage of formal modelling and analysis technology in a lightweight way, making signi cant use of readily available tools. We describe an incremental approach in which detail is progressively added to abstract system-level speci cations of functional and timing properties via intermediate models that express system architecture, concurrency and distribution. The approach is illustrated using a modelof a home automation system. The models are expressed using the Vienna Development Method (VDM) and are validated primarily by scenario-based tests.     

Early quality monitoring in the development of real-time reactive systems

The increasing trend toward complex software systems has highlighted the need to incorporate quality requirements earlier in the development cycle. We propose a new methodology for monitoring quality in the earliest phases of real-time reactive system (RTRS) development. The targeted quality characteristics are functional complexity, performance, reliability, architectural complexity, maintainability, and test coverage. All these characteristics should be continuously monitored throughout the RTRS development cycle, to provide decision support and detect the first signs of low or decreasing quality as the system design evolves. The ultimate goal of this methodology is to assist developers in dealing with complex user requirements and ensure that the formal development process yields a high-quality application. Each aspect of quality monitoring is formalized mathematically and illustrated using a train-gate-controller case study.     

某飞机辅冷系统IMA应用实时验证模型研究

某飞机环控增加蒸发制冷式辅助冷却系统(简称辅冷系统),对多个厨房、大功率电子设备以及设备舱进行冷却。为了对综合模块化航空电子系统(IMA)驻留应用进行硬件在环(HIL)测试验证,开展辅冷系统实时仿真模型研究。在对辅冷系统冷凝器等关键部件的建模原理进行数学描述后,利用MATLAB/Simulink进行部件建模与仿真分析,并根据建模框架对辅冷系统模型进行集成与仿真,最后将模型下载到实时机对IMA应用进行HIL测试。仿真与测试结果表明,制冷剂工作压焓曲线满足要求,辅冷系统模型仿真误差满足要求,可以对IMA应用进行实时的仿真验证。首次利用模型开展制冷剂在关键部件的工作压焓曲线以及飞机辅冷全系统的HIL测试研究,该研究对制冷领域的系统级实时仿真验证具有参考意义。     

基于对象分布式实时系统约束的一致性研究

在分布式实时系统中,时间约束规格的一致性是解决任务分配和调度等关键问题的必要前提。该文给出了一种基于对象分布式实时系统调度的通用模型,并对该模型进行了形式化描述。该模型克服了以往模型不能在应用系统的逻辑和功能部件上描述系统实时约束的不足,允许从方法和活动上描述所需的约束,降低了单一约束描述的繁杂程度。为了解决使用该模型进行约束规格的一致性问题,该文给出了绝对时间约束、相对时间约束、一致性约束以及相对时间约束和一致性约束之间的一致性判定的必要条件。     

基于设计演算的形式化用例分析建模框架

提出一种形式化用例分析建模框架,引入类图、用例顺序图、用例状态图、功能规约函数和系统不变式从多个角度为需求建模.通过定义这些视图的形式化语义,为需求的各个方面定义了准确的形式化描述.利用该框架,可以从方法的交互行为规约和功能规约合成描述方法全部行为的全规约;也可以定义用例模型的性质,并通过设计演算中的证明来分析验证这些性质.作为应用,研究了检查用例模型一致性的规则.给出一个实例说明建模框架的可行性.