Compiling and verifying SC-SystemJ programs for safety-critical reactive systems

Most of today's embedded systems are very complex. These systems, controlled by computer programs, continuously interact with their physical environments through network of sensory input and output devices. Consequently, the operations of such embedded systems are highly reactive and concurrent. Since embedded systems are deployed in many safety-critical applications, where failures can lead to catastrophic events, an approach that combines mathematical logic and formal verification is employed in order to ensure correct behavior of the control algorithm. This paper presents What You Prove Is What You Execute (WYPIWYE) compilation strategy for a Globally Asynchronous Locally Synchronous (GALS) programming language called Safey-Critical SystemJ. SC-SystemJ is a safety-critical subset of the SystemJ language. A formal big-step transition semantics of SC-SystemJ is developed for compiling SC-SystemJ programs into propositional Linear Temporal Logic formulas. These LTL formulas are then converted into a network of Mealy automata using a novel and efficient compilation algorithm. The resultant Mealy automata have a straightforward syntactic translation into Promela code. The resultant Promela models can be used for verifying correctness properties via the SPIN model-checker. Finally there is a single translation procedure to compile both: Promela and C/Java code for execution, which satisfies the De-Bruijn index, i.e. this final translation step is simple enough that is can be manually verified.     

Implementation of visual languages using pattern‐based specifications

The implementation of visual languages requires a wide range of conceptual and technical knowledge from issues of user interface design and graphical implementation to aspects of analysis and transformation for languages in general. We present a powerful toolset that incorporates such knowledge. Our toolset generates editors from high‐level specifications. A language is specified by identifying certain patterns in the language structure and selecting a visual representation from a set of precoined solutions. Visual programs are represented by attributed abstract trees. Therefore, further phases of processing visual programs can be generated by state‐of‐the‐art tools for language implementation. We demonstrate that even challenging visual languages can be implemented with reasonably little effort and with rather limited technical knowledge. The approach is suitable for a large variety of visual language styles. Copyright © 2003 John Wiley & Sons, Ltd.     

Toward Automated Support for Transparent Interoperable Queries

Many Object-Oriented Databases (OODBs) use programming languages that predate Java, such as C++, CLOS and Smalltalk. Thus, there is a growing need for interoperating these OODBs with new applications that require Java. Unfortunately, there are few mechanisms that allow software developers to easily integrate Java applications with non-Java OODBs. Although various interoperability mechanisms have been developed over the years, these approaches have some significant drawbacks in practice. They are often difficult to use, provide little, if any, automated support, and produce software that is difficult to engineer and maintain. In this paper, we describe an interoperability approach that allows application developers to seamlessly and transparently access non-Java OODBs from Java applications. We first present JOQL, a Java-based object query language that we are developing. JOQL queries are embedded in Java applications and are used to perform queries over C++-based OODBs. We also describe an accompanying toolset that processes Java programs containing JOQL queries. The toolset produces all the necessary code allowing Java applications to access and manipulate a C++-based OODB. As a result, application developers are free to work in Java without having to concern themselves with the details of interoperating with C++. Finally, we provide some preliminary experimental data that demonstrates our approach incurs a reasonable performance overhead.     

基于Coq的矩阵代码生成技术

矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.     

The KeY tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.     

Embedded Software Verification Using Symbolic Execution and Uninterpreted Functions

Symbolic simulation and uninterpreted functions have long been staple techniques for formal hardware verification. In recent years, we have adapted these techniques for the automatic, formal verification of low-level embedded software—specifically, checking the equivalence of different versions of assembly language programs. Our approach, though limited in scalability, has proven particularly promising for the intricate code optimizations and complex architectures typical of high-performance embedded software, such as for DSPs and VLIW processors. Indeed, one of our key findings was how easy it was to create or retarget our verification tools to different, even very complex, machines. The resulting tools automatically verified or found previously unknown bugs in several small sequences of industrial and published example code. This paper provides an introduction to these techniques and a review of our results.     

A formal approach for run-time verification of web applications using scope-extended LTL

ContextIn the past decade, the World Wide Web has been subject to rapid changes. Web sites have evolved from static information pages to dynamic and service-oriented applications that are used for a broad range of activities on a daily basis. For this reason, thorough analysis and verification of Web Applications help assure the deployment of high quality applications.ObjectivesIn this paper, an approach is presented to the formal verification and validation of existing web applications. The approach consists of using execution traces of a web application to automatically generate a communicating automata model. The obtained model is used to model checking the application against predefined properties, to perform regression testing, and for documentation.MethodsTraces used in the proposed approach are collected by monitoring a web application while it is explored by a user or a program. An automata-based model is derived from the collected traces by mapping the pages of the application under test into states and the links and forms used to browse the application into transitions between the states. Properties, meanwhile, express correctness and quality requirements on web applications and might concern all states of the model; in many cases, these properties concern only a proper subset of the states, in which case the model is refined to designate the subset of the global states of interest. A related problem of property specification in Linear Temporal Logic (LTL) over only a subset of states of a system is solved by means of specialized operators that facilitate specifying properties over propositional scopes in a concise and intuitive way. Each scope constitutes a subset of states that satisfy a propositional logic formula.ResultsAn implementation of the verification approach that uses the model checker Spin is presented where an integrated toolset is developed and empirical results are shown. Also, Linear Temporal Logic is extended with propositional scopes.Conclusiona formal approach is developed to build a finite automata model tuned to features of web applications that have to be validated, while delegating the task of property verification to an existing model checker. Also, the problem of property specification in LTL over a subset of the states of a given system is addressed, and a generic and practical solution is proposed which does not require any changes in the system model by defining specialized operators in LTL using scopes.     

The Synchronous Approach to Designing Reactive Systems

Synchronous programming is available through several formally defined languages having very different characteristics: Esterel is imperative, while Lustre and Signal are declarative in style; Statecharts and Argos are graphical languages that allow one to program by constructing hierarchical automata. Our motivation for taking the synchronous design paradigm further, integrating imperative, declarative (or dataflow), and graphical programming styles, is that real systems typically have components that match each of these profiles. This paper motivates our interest in the mixed language programming of embedded software around a number of examples, and sketches the semantical foundation of the Synchronie toolset which ensures a coherent computational model. This toolset supports a design trajectory that incorporates rapid prototyping and systematic testing for early design validation, an object oriented development methodology for long term software management, and formal verification at the level of automatically generated object code.     

Matrix representations,linear transformations,and kernels for disambiguation in natural language

In the application of machine learning methods with natural language inputs, the words and their positions in the input text are some of the most important features. In this article, we introduce a framework based on a word-position matrix representation of text, linear feature transformations of the word-position matrices, and kernel functions constructed from the transformations. We consider two categories of transformations, one based on word similarities and the second on their positions, which can be applied simultaneously in the framework in an elegant way. We show how word and positional similarities obtained by applying previously proposed techniques, such as latent semantic analysis, can be incorporated as transformations in the framework. We also introduce novel ways to determine word and positional similarities. We further present efficient algorithms for computing kernel functions incorporating the transformations on the word-position matrices, and, more importantly, introduce a highly efficient method for prediction. The framework is particularly suitable to natural language disambiguation tasks where the aim is to select for a single word a particular property from a set of candidates based on the context of the word. We demonstrate the applicability of the framework to this type of tasks using context-sensitive spelling error correction on the Reuters News corpus as a model problem.     

On construction of a library of formally verified low-level arithmetic functions

Arithmetic functions are used in many important computer programs such as computer algebra systems and cryptographic software. The latter are critical applications whose correct implementation deserves to be formally guaranteed. They are also computation-intensive applications, so that programmers often resort to low-level assembly code to implement arithmetic functions. We propose an approach for the construction of a library of formally verified low-level arithmetic functions. To build our library, we first introduce a formalization of data structures for signed multi-precision arithmetic in low-level programs. We use this formalization to verify the implementation of several primitive arithmetic functions using Separation logic, an extension of Hoare logic to deal with pointers. Since this direct style of formal verification leads to technically involved specifications, we also propose for larger functions to show a formal simulation relation between pseudo-code and assembly. This style of verification is illustrated with a concrete implementation of the binary extended gcd algorithm.     

A MATLAB subset to C compiler targeting embedded systems

This paper describes MATISSE, a compiler able to translate a MATLAB subset to C targeting embedded systems. MATISSE uses LARA, an aspect‐oriented programming language, to specify additional information and transformations to the input MATLAB code, for example, insertion of code for initialization of variables, and specification of types and shapes of variables. The compiler is being developed bearing in mind flexibility, multitarget and multitoolchain support, allowing for the generation of several implementations in C from the same reference code in MATLAB. In this paper, we also present a number of techniques being employed in MATLAB to C compilation, such as element‐wise mapping operations, matrix views, weak types, and intrinsics. We validate these techniques using MATISSE and a set of representative benchmarks. More specifically, we evaluate the compiler with a set of 31 benchmarks using an embedded system board and a desktop computer. The results show speedups up to 1.8× by employing information provided by LARA aspects, when compared with C code generated without additional user information. When compared with the execution time of the original code running on MATLAB, the execution time of the generated C code achieved a geometric mean speedup of 13×. Copyright © 2016 John Wiley & Sons, Ltd.     

Validation of static properties in unified modeling language models for cyber physical systems

Cyber physical systems (CPSs) can be found nowadays in various fields of activity. The increased interest for these systems as evidenced by the large number of applications led to complex research regarding the most suitable methods for design and development. A promising solution for specification, visualization, and documentation of CPSs uses the Object Management Group (OMG) unified modeling language (UML). UML models allow an intuitive approach for embedded systems design, helping end-users to specify the requirements. However, the UML models are represented in an informal language. Therefore, it is difficult to verify the correctness and completeness of a system design. The object constraint language (OCL) was defined to add constraints to UML, but it is deficient in strict notations of mathematics and logic that permits rigorous analysis and reasoning about the specifications. In this paper, we investigated how CPS applications modeled using UML deployment diagrams could be formally expressed and verified. We used Z language constructs and prototype verification system (PVS) as formal verification tools. Considering some relevant case studies presented in the literature, we investigated the opportunity of using this approach for validation of static properties in CPS UML models.     

Efficient relational calculation for software analysis

Calculating with graphs and relations has many applications in the analysis of software systems, for example, the detection of design patterns or patterns of problematic design and the computation of design metrics. These applications require an expressive query language, in particular, for the detection of graph patterns, and an efficient evaluation of the queries even for large graphs. In this paper, we introduce RML, a simple language for querying and manipulating relations based on predicate calculus, and CrocoPat, an interpreter for RML programs. RML is general because it enables the manipulation not only of graphs (i.e., binary relations), but of relations of arbitrary arity. CrocoPat executes RML programs efficiently because it internally represents relations as binary decision diagrams, a data structure that is well-known as a compact representation of large relations in computer-aided verification. We evaluate RML by giving example programs for several software analyses and CrocoPat by comparing its performance with calculators for binary relations, a Prolog system, and a relational database management system.     

Enriching MATLAB with aspect-oriented features for developing embedded systems

This article presents an approach to enrich the MATLAB¹ language with aspect-oriented modularity features, enabling developers to experiment different implementation characteristics and to acquire runtime data and traces without polluting their base MATLAB code. We propose a language through which programmers configure the low-level data representation of variables and expressions. Examples include specifically-tailored fixed-point data representations leading to more efficient support for the underlying hardware, e.g., digital signal processors and application-specific architectures, without built-in floating point units. This approach assists developers in adding handlers and monitoring features in a non-invasive way as well as configuring MATLAB functions with optimized implementations. Different aspect modules can be used to retarget common MATLAB code bases for different purposes and implementations. We validate the proposed approach with a set of representative examples where we attain a simple way to explore a number of properties. Experiment results and collected aspect-oriented software metrics lend support to the claims on its usefulness.     

A configuration approach to parallel programming

This paper advocates a configuration approach to parallel programming for distributed memory multicomputers, in particular, arrays of transputers. The configuration approach prescribes the rigorous separation of the logical structure of a program from its component parts. In the context of parallel programs, components are processes which communicate by exchanging messages. The configuration defines the instances of these processes which exist in the program and the paths by which they are interconnected.

The approach is demonstrated by a toolset (Tonic) which embodies the configuration paradigm. A separate configuration language is used to describe both the logical structure of the parallel program and the physical structure of the target multicomputer. Different logical to physical mappings can be obtained by applying different physical configurations to the same logical configuration. The toolset has been developed from the Conic system for distributed programming. The use of the toolset is illustrated through its application to the development of a parallel program to compute Mandelbrot sets.     

Dempster–Shafer evidential theory for the automated selection of parameters for Talbot’s method contours and application to matrix exponentiation

In this paper, the Dempster–Shafer theory of evidential reasoning is applied to the problem of optimal contour parameters selection in Talbot’s method for the numerical inversion of the Laplace transform. The fundamental concept is the discrimination between rules for the parameters that define the shape of the contour based on the features of the function to invert. To demonstrate the approach, it is applied to the computation of the matrix exponential via numerical inversion of the corresponding resolvent matrix. Training for the Dempster–Shafer approach is performed on random matrices. The algorithms presented have been implemented in MATLAB. The approximated exponentials from the algorithm are compared with those from the rational approximation for the matrix exponential returned by the MATLAB expm function.     

Automated Verification of Functional Correctness of Race-Free GPU Programs

We study an automated verification method for functional correctness of parallel programs running on graphics processing units (GPUs). Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop invariants, and passes them to off-the-shelf SMT solvers. It is often impossible, however, to solve naively generated VCs in reasonable time. A main difficulty stems from quantifiers over threads due to the parallel nature of GPU programs. To overcome this difficulty, we additionally apply several transformations to simplify VCs before calling SMT solvers. Our implementation successfully verifies correctness of several GPU programs, including matrix multiplication optimized by using shared memory. In contrast to many existing verification tools for GPU programs, our verifier succeeds in verifying fully parameterized programs: parameters such as the number of threads and the sizes of matrices are all symbolic. We empirically confirm that our simplification heuristics is highly effective for improving efficiency of the verification procedure.     

时序逻辑语言XYZ/E中指针的形式化表示与验证

指针是一种重要的数据类型,使用指针能使程序更加有效和优美.可是指针却以不易驾御而闻名,至今在时序逻辑语言中未见到对它的形式化工作.XYZ/E既是一个时序逻辑系统也是一个程序设计语言,它能表示普通高级语言中几乎所有的重要机制.本文主要讨论在时序逻辑语言XYZ/E中指针的形式化表示问题以及在结构化XYZ/SE程序中指针的验证问题.     

Automatic library migration for the generation of hardware-in-the-loop models

Embedded systems are widely used in several applications nowadays. As they integrate hard- and software elements, their functionality and reliability are often tested by hardware-in-the-loop methods, in which the system under test runs in a simulated environment. Due to the rising complexity of the embedded functions, performance limitations and practicability reasons, the simulations are often specialized to test specific aspects of the embedded system and develop a high diversity by themselves. This diversity is difficult to manage for a user and results in erroneously selected test components and compatibility problems in the test configuration. This paper presents a generative programming approach that handles the diversity of test libraries. Compatibility issues are explicitly evaluated by a new interface concept. Furthermore, a novel model analyzer facilitates the efficient application in practice by migrating existing libraries. The approach is evaluated for an example from the automotive domain using MATLAB/Simulink.     

Towards verification of C# programs: A three-level approach

In the paper, a new three-level approach to the verification of sequential object-oriented programs is presented. It is applied to an expressive subset C#-light of the C# language, which includes all basic sequential constructs of the latter. At the first stage, the C#-light language is translated into the intermediate C#-kernel language. At the second stage, lazy correctness conditions are generated by means of the axiomatic semantics developed for C#-kernel. These conditions are lazy because they may include special functional symbols representing postponed extraction of invariants of labeled statements, as well as postponed invocations of methods and delegates. At the third stage, these conditions are refined with the use of operational semantics algorithms. Such an approach simplifies the axiomatic semantics and makes it possible to uniquely derive correctness conditions. An example of verification of a C#-light program is presented.