VERTAF: an application framework for the design and verification of embedded real-time software

The growing complexity of embedded real-time software requirements calls for the design of reusable software components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties such as performance, time constraints, reliability, and security. Available application frameworks targeted at the automatic design of embedded real-time software are poor in integrating functional and nonfunctional requirements. To bridge this gap, we reveal the design flow and the internal architecture of a newly proposed framework called verifiable embedded real-time application framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time object model is proposed for component reuse. Formal synthesis employs quasistatic and quasidynamic scheduling with automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. The proposed architecture for VERTAF is component-based and allows plug-and-play for the scheduler and the verifier. Using VERTAF to develop application examples significantly reduced design effort and illustrated how high-level reuse of software components combined with automatic synthesis and verification can increase design productivity.     

基于组件的嵌入式软件开发方法

根据嵌入式软件的特点，提出一种以模型为中心、基于组件的嵌入式软件开发方法。它以动态数据流图为系统模型对嵌入式软件的功能和性能需求进行了描述，由此提供了强大的描述和分析能力；通过基于特定组件模型的实现结构和实现代码框架的自动生成，以DDF定义的系统可以被有效地分解为一系列独立的组件，合适的DDF调度算法一致地表示了系统组件的执行语义，使得并发开发的组件具有良好的可集成性。该方法充分考虑了嵌入式开发的特点，能有效地降低系统复杂性和支持系统组件的并发开发和复用，从而提高了开发效率并降低了开发成本。     

Formal Methods in Designing Embedded Systems—the SACRES Experience

From automotive electronics to avionics, embedded systems are part of our everyday life, and developed societies are increasingly dependent on their reliability in operation. At the same time, current design practice is inadequate in coping with the challenge of constructing dependable embedded systems.SACRES is an experimental design environment aimed at the seamless development of embedded systems. It incorporates state-of-the-art industrial design tools and provides formal specification, model checking technology and validated code generation. These concepts have been integrated on the basis of the synchronous approach to reactive systems.As a result, synchronous compilation techniques have been enhanced, in particular as regards techniques for distributed code generation. Formal verification technology was advanced to increase efficiency, handle composed systems and cover some real-time aspects. The new approach of translation validation was developed and proven to work.Real bugs have been found even in well-tested models. It was demonstrated that a formal design including verification is often more efficient than testing. As a consequence, all user partners are committed to further introducing formal design and verification technology.This paper summarises the essential achievements of the project. It explains the results in terms of the basic ideas, the available tools and methodology, as well as the experience gained.     

Design verification in model-based?��-controller development using an abstract component

Component-based software development is a promising approach for controlling the complexity and quality of software systems. Nevertheless, recent advances in quality control techniques do not seem to keep up with the growing complexity of embedded software; embedded systems often consist of dozens to hundreds of software/hardware components that exhibit complex interaction behavior. Unanticipated quality defects in a component can be a major source of system failure. To address this issue, this paper suggests a design verification approach integrated into the model-driven, component-based development methodology Marmot. The notion of abstract components—the basic building blocks of Marmot—helps to lift the level of abstraction, facilitates high-level reuse, and reduces verification complexity by localizing verification problems between abstract components before refinement and after refinement. This enables the identification of unanticipated design errors in the early stages of development. This work introduces the Marmot methodology, presents a design verification approach in Marmot, and demonstrates its application on the development of a μ-controller-based abstraction of a car mirror control system. An application on TinyOS shows that the approach helps to reuse models as well as their verification results in the development process.     

在构件化嵌入式操作系统中应用抢占阈值调度

现有基于构件的嵌入式实时软件开发过程着重于从结构的角度分解系统成若干构件,以及重用构件。实践证明,该开发过程还应从运行角度将构件映射成任务,并选择适当的实时调度算法。为此,根据目前的工程实践提出一种实时构件模型,包含将构件映射成任务的方式。描述了当前构件化嵌入式操作系统可以使用的4种调度算法,并比较这些算法的性能特点。提出抢占阈值(preemptionthreshold)调度模型更适合构件化嵌入式实时系统,仿真实验的结果证明了该结论。比较结果和结论对构件化嵌入式实时系统的设计和开发有一定的参考价值。     

嵌入式软件建模、实现与验证：研究与进展

随着计算机硬件设备计算能力的迅速提高,嵌入式系统中软件的规模和复杂度的急剧增大,软件可靠性在嵌入式系统中的重要性占据了统治地位。本文首先概要介绍了嵌入式软件不同于传统商业软件、科学计算软件的物理性、实时性、领域性等重要特征,以及由此带来的困难和挑战。然后重点介绍目前在解决嵌入式软件系统开发过程中的问题时所采取的建模思想、实现技术和验证方法。最后对嵌入式软件及其相关技术的发展进行了展望。     

Integrating UML and UPPAAL for designing, specifying and verifying component-based real-time systems

A new tool for integrating formal methods, particularly model checking, in the development process of component-based real-time systems specified in UML is proposed. The described tool, TANGRAM (Tool for Analysis of Diagrams), performs automatic translation from UML diagrams into timed automata, which can be verified by the UPPAAL model checker. We focus on the CORBA Component Model. We demonstrate the overall process of our approach, from system design to verification, using a simple but real application, used in train control systems. Also, a more complex case study regarding train control systems is described.     

一种基于嵌入式软件构件管理方法

构件化软件开发的最终目的是希望软件像传统产品一样能在生产线上生产出来。软件最终由软件框架来实现,一个良好的软件框架应该能够将设计结果尽量保存下来,同时可以灵活更换和重用软件部件。研究构件化的软件框架对构件化的开发技术在嵌入式实时软件开发中迅速普及具有最直接的推动作用。对嵌入式控制系统嵌入软件构件框架进行了深入研究,完成了框架中的数据管理和构件调度机制等内容,验证了该源码构件模型在嵌入式控制软件领域中的可用性。     

智能家电嵌入式软件的源码构件设计方法

通过对家电控制器常用MCU体系结构、程序设计语言、家电功能及外设驱动源码研究，提出了一种形式化的嵌入式软件的源码构件和程序代码的设计方法。介绍了源码构件层次体系和逻辑模式；定义了源码构件运算符；给出了构件及应用代码的形式化生成；并以重用因子K为标准，辅助衡量源码构件的代码片段划分和设计的合理性。该方法具有很好的实用性、可扩展性和通用性。     

Verifying distributed real-time properties of embedded systems via graph transformations and model checking

Component middleware provides dependable and efficient platforms that support key functional, and quality of service (QoS) needs of distributed real-time embedded (DRE) systems. Component middleware, however, also introduces challenges for DRE system developers, such as evaluating the predictability of DRE system behavior, and choosing the right design alternatives before committing to a specific platform or platform configuration. Model-based technologies help address these issues by enabling design-time analysis, and providing the means to automate the development, deployment, configuration, and integration of component-based DRE systems. To this end, this paper applies model checking techniques to DRE design models using model transformations to verify key QoS properties of component-based DRE systems developed using Real-time CORBA. We introduce a formal semantic domain for a general class of DRE systems that enables the verification of distributed non-preemptive real-time scheduling. Our results show that model-based techniques enable design-time analysis of timed properties and can be applied to effectively predict, simulate, and verify the event-driven behavior of component-based DRE systems. This research was supported by the NSF Grants CCR-0225610 and ACI-0204028 Gabor Madl is a Ph.D. student and a graduate student researcher at the Center for Embedded Computer Systems at the University of California, Irvine. His advisor is Nikil Dutt. His research interests include the formal verification, optimization, component-based composition, and QoS management of distributed real-time embedded systems. He received his M.S. in computer science from Vanderbilt University and in computer engineering from the Budapest University of Technology and Economics. Dr. Sherif Abdelwahed received his Ph.D. degree in Electrical and Computer Engineering from the University of Toronto, Canada, in 2001. During 2000–2001, he was a research scientist with the system diagnosis group at the Rockwell Scientific Company. Since 2001 he has been with the Department of Electrical Engineering and Computer Science at Vanderbilt University as a Research Assistant Professor. His research interests include verification and control of distributed real-time systems, and model-based diagnosis of discrete-event and hybrid systems. Dr. Douglas C. Schmidt is a Professor of Computer Science, Associate Chair of the Computer Science and Engineering program, and a Senior Researcher in the Institute for Software Integrated Systems (ISIS) all at Vanderbilt University. He has published over 300 technical papers and 6 books that cover a range of research topics, including patterns, optimization techniques, and empirical analyses of software frameworks and domain-specific modeling environments that facilitate the development of distributed real-time and embedded (DRE) middleware and applications. Dr. Schmidt has served as a Deputy Office Director and a Program Manager at DARPA, where he lead the national R&D effort on middleware for DRE systems. In addition to his academic research and government service, Dr. Schmidt has over fifteen years of experience leading the development of ACE, TAO, CIAO, and CoSMIC, which are widely used, open-source DRE middleware frameworks and model-driven tools that contain a rich set of components and domain-specific languages that implement patterns and product-line architectures for high-performance DRE systems.     

Modeling and simulation-driven development of embedded real-time systems

The design and development of embedded hard real-time (RT) systems is one of the complex development practices, because of the requirements of criticality and timeliness of these systems. One critical aspect of RT systems is the production of output before specified deadline. Formal methods are promising in dealing with the design issues of these applications, although they do not scale well for complex systems. Instead, Modeling and Simulation (M&S) provides a cost-effective approach to verify the design and implementation details of very Complex RT applications. M&S methods provide dynamic and risk-free testing environments to verify different scenarios, and they are used for feasibility analysis and verification of such systems. Nevertheless, the simulation models are usually discarded in the later phases of the development.We present the application of an M&S-based method referred to as DEVSRT (Discrete EVent System Specifications in Real-Time) to solve the discontinuity between the simulation models and the final embedded application, in this paper. DEVSRT defines explicit deadline notation for DEVS transitions, draws a clear mapping between DEVS transitions and real-time tasks and provides a formal method and tool for integration of simulation models with the associated hardware components.     

Formal component-based modeling and synthesis for PLC systems

Programmable Logic Controllers (PLCs) are widely used in industry. PLC systems are reactive systems which run cyclically. In each cycle, the system state is checked and the program is executed once to determine the system behavior for a single cycle. Development of PLC systems conventionally follows the V-model, but increasing demand for efficiency and reliability requires a new rigorous and rapid design flow. In this paper, we propose a component-based formal modeling and synthesis method for cyclic execution platforms and apply it to PLC. Our method consists of three main phases: modeling, verification and code synthesis. In the modeling phase, the BIP (Behavior–Interaction–Priority) framework which is flexible and expressive is used as the modeling language. Real-time behavior, which is intensely concerned in PLC systems, can be modeled as well. In the verification phase, the system model is translated to timed automata and checked by Uppaal. Verification helps to ensure correctness of the model and further increases reliability of the implementation. In the code synthesis phase, the software part of the system model is extracted and synthesized to cyclic code. Although the PLC software runs cyclically, the software model is not necessarily given in a cyclic manner. We propose an algorithm which can generate high-performance cyclic code from a model which describes the business work-flow. This feature significantly simplifies program development. A set of tools is implemented to support our design flow and they are applied to an industrial case study for a PLC system that controls dozens of physical devices in a huge palace.     

基于动态数据流图的嵌入式系统设计

该文提出一种嵌入式系统软硬件协同设计方法,它以动态数据流图为系统模型对嵌入式系统的功能和性能需求进行描述,由此提供强大的描述、分析能力及可接受的实现规模.通过一种特定的实现结构,以及数据通路的自动综合和实现代码框架的自动生成,设计工作的主体部分可以被有效分解为一系列独立设计任务,能缩短设计周期并提高设计工作的可重用性。     

Models and temporal logical specifications for timed component connectors

Component-based software engineering advocates construction of software systems through composition of coordinated autonomous components. Significant benefits of this approach include software reuse, simpler and faster construction, enhanced reliability, and dramatic reductions in the complexity of construction of provably correct critical systems, many of which involve real-time concerns. Effective, flexible component composition by itself still poses a challenge today and yet the special nature of real-time constraints makes component-based construction of real-time systems even more demanding. The coordination language Reo supports compositional system construction through connectors that exogenously coordinate the interactions among the constituent components which unawarely comprise a complex system, into a coherent collaboration. The simple, yet surprisingly rich, calculus of channel composition that underlies Reo offers a flexible framework for compositional construction of coordinating component connectors with real-time properties. In this paper, we present an operational semantics for the channel-based component connectors of Reo in terms of Timed Constraint Automata and introduce a temporal-logic for specification and verification of their real-time properties.      

基于C/S关系的实时系统构件交互规约

给出了基于构件的实时多任务应用系统图形化设计软件的构件接口定义。为解决基于构件的分布式C/S关系的实时软件构件的重用及装配问题,提出了构件相互交互的文本描述语言语法语义规约,其主要刻画了分布式实时构件之间的交互协议及其实时特性。     

The KlaperSuite framework for model-driven reliability analysis of component-based systems

Automatic prediction tools play a key role in enabling the application of non-functional requirements analysis, to simplify the selection and the assembly of components for component-based software systems, and in reducing the need for strong mathematical skills for software designers. By exploiting the paradigm of Model-Driven Engineering (MDE), it is possible to automatically transform design models into analytical models, thus enabling formal property verification. MDE is the core paradigm of the KlaperSuite framework presented in this paper, which exploits the KLAPER pivot language to fill the gap between design and analysis of component-based systems for reliability properties. KlaperSuite is a family of tools empowering designers with the ability to capture and analyze quality of service views of their systems, by building a one-click bridge towards a number of established verification instruments. In this article, we concentrate on the reliability-prediction capabilities of KlaperSuite and we evaluate them with respect to several case studies from literature and industry.     

基于服务连接和消息连接软件构架的研究

软件构架是解决复杂大型软件开发面临的困难，提高软件质量和软件生产效率的有效方法，是软件复用和基于构件软件工程研究的重要领域，通过对软件构架风格特点的讨论和对构件之间交互方式的分析，论文提出了基于服务连接和消息连接的软件构架风格，开发了一个支持该构架风格的构件生产和组装平台，该构架风格具有以下特点，（1）支持多种可变性机制；（2）构件之间灵活和显式的服务连接和消息连接机制；（3）支持构件合成；（4）构件接口分组，成为端口。     

The SDL pattern approach – a reuse-driven SDL design methodology

There are several SDL methodologies that offer full system life-cycle support. Only few of them consider software reuse, not to mention high-level reuse of architecture and design. However, software reuse is a proven software engineering paradigm leading to high quality and reduced development effort. Experience made it apparent that – beyond the more traditional reuse of code – especially high-level reuse of architecture and design (as in the case of design patterns or frameworks) has the potential of achieving more systematic and widespread reuse. This paper presents the SDL pattern approach, a design methodology for distributed systems which integrates SDL-based system development with the pattern paradigm. It supports reuse of design knowledge modeled as SDL patterns and concentrates on the design phase of SDL-based system development. In order to get full life-cycle support, the pattern-based design process can be integrated within existing SDL methodologies.