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.     

Runtime verification of concurrency-specific correctness criteria

We give an overview of correctness criteria specific to concurrent shared-memory programs and runtime verification techniques for verifying these criteria. We cover a spectrum of criteria, from ones focusing on low-level thread interference such as races to higher-level ones such as linearizability. We contrast these criteria in the context of runtime verification. We present the key ideas underlying the runtime verification techniques for these criteria and summarize the state of the art. Finally, we discuss the issue of coverage for runtime verification for concurrency and present techniques that improve the set of covered thread interleavings.     

A functional correctness model of program verification

A model whose verification conditions depend only on elementary symbolic execution of a trace table is presented. The method is applied to rather simple programs. However, even in large complex implementations, the techniques can be applied informally to determine the functionality of complex interactions. The technique is easy to learn (it is used in a freshman computer science course) and lends itself to automation     

The case for electric design of real-time software

G. Booch (see ibid., vol.SE-12, no.2, p.211-21, Feb. 1986) has analyzed a problem involving the software of a set of free-floating buoys. The correspondence points out that Booch's analysis fails to address one important system issue, namely the fact that the software must support two concurrent activities, and shows that an analysis according to the M.A. Jackson method will reveal this difficulty at an early design stage. On the other hand, the Jackson approach does not deal with some configuration issues, which are handled in Booch's analysis. This shows that one method is sometimes not enough to address all important, systemwide aspects of a problem. Rather than arguing about which one design method is best, the author recommends taking an electric view and using any combination of approaches that yields important results in a given situation     

Automating correctness verification of artifact-centric business process models

ContextThe artifact-centric methodology has emerged as a new paradigm to support business process management over the last few years. This way, business processes are described from the point of view of the artifacts that are manipulated during the process.ObjectiveOne of the research challenges in this area is the verification of the correctness of this kind of business process models where the model is formed of various artifacts that interact among them.MethodIn this paper, we propose a fully automated approach for verifying correctness of artifact-centric business process models, taking into account that the state (lifecycle) and the values of each artifact (numerical data described by pre and postconditions) influence in the values and the state of the others. The lifecycles of the artifacts and the numerical data managed are modeled by using the Constraint Programming paradigm, an Artificial Intelligence technique.ResultsTwo correctness notions for artifact-centric business process models are distinguished (reachability and weak termination), and novel verification algorithms are developed to check them. The algorithms are complete: neither false positives nor false negatives are generated. Moreover, the algorithms offer precise diagnosis of the detected errors, indicating the execution causing the error where the lifecycle gets stuck.ConclusionTo the best of our knowledge, this paper presents the first verification approach for artifact-centric business process models that integrates pre and postconditions, which define the behavior of the services, and numerical data verification when the model is formed of more than one artifact. The approach can detect errors not detectable with other approaches.     

嵌入式实时多任务软件的软总线结构设计

本文提出在嵌入式实时操作系统上建立实时多任务软件系统时,使用软总线提供数据驱动层以处理多任务间共享资源的构架方式.该方案封装各种共享资源的操作,在操作系统上构建使资源对于其他系统任务模块构建者透明的数据驱动接口.实验结果表明该方案能较好的为各任务进程提供共享资源建立和使用的接口,同时有效地屏蔽由于进程资源共享与进程独立性的矛盾而可能产生的错误.     

Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

Currently available application frameworks that target the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates three techniques namely software component-based reuse, formal synthesis, and formal verification. Component reuse is based on a formal unified modeling language (UML) real-time embedded object model. Formal synthesis employs quasi-static and quasi-dynamic scheduling with multi-layer portable efficient code generation, which can output either real-time operating systems (RTOS)-specific application code or automatically generated real-time executive with application code. Formal verification integrates a model checker kernel from state graph manipulators (SGM), by adapting it for embedded software. The proposed architecture for VERTAF is component-based which allows plug-and-play for the scheduler and the verifier. The architecture is also easily extensible because reusable hardware and software design components can be added. Application examples developed using VERTAF demonstrate significantly reduced relative design effort as compared to design without VERTAF, which also shows how high-level reuse of software components combined with automatic synthesis and verification increases design productivity.     

Deductive software verification

Deductive software verification, also known as program proving, expresses the correctness of a program as a set of mathematical statements, called verification conditions. They are then discharged using either automated or interactive theorem provers. We briefly review this research area, with an emphasis on tools.     

Hierarchical timing verification system

A hierarchical timing verification system, based on critical path analysis technique, is described. These techniques permit the system to identify the critical paths of the logic designs. The system performs timing analysis on VLSI designs with sequential circuits and feedback loops. The system traces the design both in the forward and backward directions and computes the arrival times and required arrival times at the primary inputs and primary outputs of the design. The results are applicable to hierarchical VLSI design methodologies. This system has been tested using the logic of Sperry's 1100 series mainframe computer system.     

BDD-based software verification

In software model checking, most successful symbolic approaches use predicates as representation of the state space, and SMT solvers for computations on the state space; BDDs are often used as auxiliary data structure. Although BDDs are applied with great success in hardware verification, BDD representations of software state spaces were not yet thoroughly investigated, mainly because not all operations that are needed in software verification are efficiently supported by BDDs. We evaluate the use of a pure BDD representation of integer values, and focus on a particular class of programs: event-condition-action (ECA) programs with limited operations. A symbolic representation using BDDs seems appropriate for ECA programs under certain conditions. We configure a program analysis based on BDDs and experimentally compare it to four approaches to verify reachability properties of ECA programs: an explicit-value analysis, a symbolic bounded-loops analysis, a predicate-abstraction analysis, and a predicate-impact analysis. The results show that BDDs are efficient for a restricted class of programs, which yields the insight that BDDs could be used selectively for variables that are restricted to certain program operations (according to the variable’s domain type), even in general software model checking. We show that even a naive portfolio approach, in which after a pre-analysis either a BDD-based analysis or a predicate-impact analysis is performed, outperforms all above-mentioned analyses.     

基于XYZ/SE的软件部分正确性验证

针对软件形式化描述和正确性验证研究中存在的问题,提出了基于XYZ/SE的统一框架研究该问题。在该框架下,基于逐步求精思路对软件进行抽象;对软件整体进行形式化描述和部分正确性验证;对抽象得到的软件各部分进行形式化描述和部分正确性验证;进行调整和验证,即：如果推导结果与预期不一致,则需要重写相关程序或者回溯检查推导过程是否存在错误,直至程序部分正确性得到验证为止。以国库信息处理系统为对象,分析了基于XYZ/SE的统一框架性能。分析表明,基于该框架能够对软件的不同抽象层次进行规范描述,实现从抽象（静态语义）到具体（动态语义）的平滑过渡。同时,基于XYZ/SE的统一框架也可以表示Hoare逻辑推演规则。     

基于ARM的远程实时心电监护仪软件设计实现

当前心电监护仪器主要仍然应用于传统床头静态监护,缺乏便携性和诊断全面性.提出了一种通讯基于CDMA无线网络的远程心电实时监护系统中监护仪前端的软件设计方案,整体设计立足于动态监护方式.监护仪在硬件上采用ARM7的主控芯片,通过模块化的嵌入式软件设计方案,特别在采样转换、数据存取和通讯协议方面得到细节性的实际研究,确保数据的完整性、连续性和准确性,便于监护服务器的分析诊断.监护仪还定义了人机交互接口,方便功能扩展.临床结果表明,该系统满足了动态心电监护要求.     

A framework for the design and verification of software measurement methods

At the core of any engineering discipline is the use of measures, based on ISO standards or on widely recognized conventions, for the development and analysis of the artifacts produced by engineers. In the software domain, many alternatives have been proposed to measure the same attributes, but there is no consensus on a framework for how to analyze or choose among these measures. Furthermore, there is often not even a consensus on the characteristics of the attributes to be measured.In this paper, a framework is proposed for a software measurement life cycle with a particular focus on the design phase of a software measure. The framework includes definitions of the verification criteria that can be used to understand the stages of software measurement design. This framework also integrates the different perspectives of existing measurement approaches. In addition to inputs from the software measurement literature the framework integrates the concepts and vocabulary of metrology. This metrological approach provides a clear definition of the concepts, as well as the activities and products, related to measurement. The aim is to give an integrated view, involving the practical side and the theoretical side, as well as the basic underlying concepts of measurement.     

基于ε-互模拟的软件近似正确性模型

软件正确性是软件可信性的重要属性。在实际软件开发和设计中,需要不断地对软件进行修改,从而软件越来越正确。为了讨论软件的动态近似正确性,基于概率进程代数的ε-互模拟,建立软件越来越正确的形式化描述。定义ε-极限互模拟,用来反应软件实现与规范之间的关系,给出一些特殊的ε-极限互模拟。提出ε-互模拟极限,用其刻画规范是软件实现的极限形式,同时证明ε-互模拟极限的一些性质。     

A design flow for supporting component-based software development in multiprocessor real-time systems

Component-based software development established as an effective technique to cope with the increasing complexity of modern computing systems. In the context of real-time systems, the M-BROE framework has been recently proposed to efficiently support component-based development of real-time applications on multiprocessor platforms in the presence of shared resources. The framework relies on a two-stage approach where software components are first partitioned upon a virtual multiprocessor platform and are later integrated upon the physical platform by means of component interfaces that abstract from the internal details of the applications. This work presents a complete design flow for the M-BROE framework. Starting from a model of software components, a first method is proposed to partition applications to virtual processors and perform a synthesis of multiple component interfaces. Then, a second method is proposed to support the integration of the components by allocating virtual processors to physical processors. Both methods take resource sharing into account. Experimental results are also presented to evaluate the proposed methodology.     

A framework for determining design correctness

Quality is one of the main concerns in today's systems and software development and use. One important instrument in verification is the use of formal methods, which means that requirements and designs are analyzed formally to determine their relationships. Furthermore, since professional software design is to an increasing extent a distributed process, the issue of integrating different systems to an entity is of great importance in modern system development and design. Various candidates for formalizing system development and integration have prevailed, but very often, particularly for dynamic conflict detection, these introduce non-standard objects and formalisms, leading to severe confusion, both regarding the semantics and the computability. In contrast to such, we introduce a framework for defining requirement fulfillment by designs, detecting conflicts of various kinds as well as integration of heterogeneous schemata. The framework introduced transcends ordinary logical consequence, as it takes into account static and dynamic aspects of design consistency and, in particular, the specific features of the state space of a specification. Another feature of the approach is that it provides a unifying framework for design conflict analysis and schema integration.     

Tools for software verification

Developing tools that are able to perform automatic verification on realistic models of software systems is one of the main challenges facing the formal methods community. We briefly review the research area and introduce three papers selected from the Seventeenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (tacas 2011).     

Embedded software verification in hardware–software codesign

Concurrent Embedded Real-Time Software (CERTS) is intrinsically different from traditional, sequential, independent, and temporally unconstrained software. The verification of software is more complex than hardware due to inherent flexibilities (dynamic behavior) that incur a multitude of possible system states. The verification of CERTS is all the more difficult due to its concurrency and embeddedness. The work presented here shows how the complexity of CERTS verification can be reduced significantly through answering common engineering questions such as when, where, and how one must verify embedded software. First, a new Schedule-Verify-Map strategy is proposed to answer the when question. Second, verification under system concurrency is proposed to answer the where question. Finally, a complete symbolic model checking procedure is proposed for CERTS verification. Several application examples illustrate the usefulness of our technique in increasing verification scalability.