An integrated system for optimal structural synthesis and remodelling

The paper presents an integrated system approach to efficient structural synthesis. It is based on a production analysis program (EAL), two general purpose optimization programs (CONMIN and NEWSUMT) and several problem-independent processors (some available with PARS and a few recently developed on EAL). The approach makes it possible to resize structures which can be “generically” modelled. The paper describes the advantages of following this integrated approach, the process of incorporating PARS (Programs for Analysis and Resizing of Structures) into EAL (Engineering Analysis Language) to form EAL/PARS and some of its newly added capabilities. An advanced synthesis system with enhanced generality and flexibility is achieved by taking advantage of the EAL higher order language commands and data base. The EAL modular structure and the ease with which new processors can be added to EAL make this system potentially adaptable to a wide spectrum of structural optimization problems.     

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.     

Dependent Types for Program Termination Verification

Program termination verification is a challenging research subject of significant practical importance. While there is already a rich body of literature on this subject, it is still undeniably a difficult task to design a termination checker for a realistic programming language that supports general recursion. In this paper, we present an approach to program termination verification that makes use of a form of dependent types developed in Dependent ML (DML), demonstrating a novel application of such dependent types to establishing a liveness property. We design a type system that enables the programmer to supply metrics for verifying program termination and prove that every well-typed program in this type system is terminating. We also provide realistic examples, which are all verified in a prototype implementation, to support the effectiveness of our approach to program termination verification as well as its unobtrusiveness to programming. The main contribution of the paper lies in the design of an approach to program termination verification that smoothly combines types with metrics, yielding a type system capable of guaranteeing program termination that supports a general form of recursion (including mutual recursion), higher-order functions, algebraic datatypes, and polymorphism.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.     

Automatic verification of Java programs with dynamic frames

Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution to this problem. However, the approach is formalized in the context of an idealized logical framework. In particular, it is not clear the solution is suitable for use within a program verifier for a Java-like language based on verification condition generation and automated, first-order theorem proving. In this paper, we demonstrate that the dynamic frames approach can be integrated into an automatic verifier based on verification condition generation and automated theorem proving. The approach has been proven sound and has been implemented in a verifier prototype. The prototype has been used to prove correctness of several programming patterns considered challenging in related work.     

A continuation‐based task programming model for C++: design of the Causeway library

There is a big class of problems that requires writing programs in an asynchronous manner. Cloud computing, service‐oriented architectures, multi‐core and heterogeneous systems all require programs to be written with asynchronous components. The necessity of concurrency and asynchronous execution brings in the added complexity of the inversion of control into the system, either through message passing or through event processing. In this paper, we introduce explicit programming language support for asynchronous programming that completely hides inversion of control. The presented programming model defines a common abstraction of the different types of tasks, both synchronous and asynchronous. It defines common imperative control constructs equivalent to those of the host programming language, along with a few more advanced ones for transactional and parallel execution that can universally work for any task type. It allows the programmer to implement the logic of an asynchronous system in a natural way by writing simple, seemingly, synchronous imperative code. We will show that the programs written using this approach are easier to understand by programmers. They are also easier to design automated tests for, and for performing computer‐based static analysis of the program logic. The principles behind this approach were tested in a couple of real‐world systems with worldwide user base. Our experience shows that it makes the complex code with a lot of interdependencies between asynchronously executed tasks easy to write and reason about. Copyright © 2016 John Wiley & Sons, Ltd.     

C-programs verification based on mixed axiomatic semantics

The mixed axiomatic semantics of the C-kernel language is described. This language is the kernel of a representative subset which is called C-light. Such semantics makes possible for the verification conditions to be simplified in many cases. The semantics is the basis of the verification conditions generator for C-kernel programs. An example illustrating the application of the inference rules of the semantics is considered.     

Sound refactorings

Refactoring consists in restructuring an object-oriented program without changing its behaviour. In this paper, we present refactorings as transformation rules for programs written in a refinement language inspired on Java that allows reasoning about object-oriented programs and specifications. A set of programming laws is available for the imperative constructs of this language as well as for its object-oriented features; soundness of the laws is proved against a weakest precondition semantics. The proof that the refactoring rules preserve behaviour (semantics) is accomplished by the application of these programming laws and data simulation. As illustration of our approach to refactoring, we use our rules to restructure a program to be in accordance with a design pattern.     

CILinear:一个线性不变式自动构造工具

构造不变式是程序验证的重要组成部分,而开源工具Interpro。能对简单的程序设计语言构造线性不变式。基于Interproc和C程序编译工具CII,针对简化的C程序设计并实现了自动构造数值型程序变量线性不变式的工具CILinear,并与Interproc进行了比较。实验表明CILinear能有效地构造线性不变式,并且比Interproc支持的语法更多。通过实例讨论了CILinear在程序验证中的实际应用。     

Validation of array accesses: integration of flow analysis and program verification techniques

A program that accesses an out-of-bound array element can cause unexpected behaviour that is unacceptable to safety-critical or security-critical systems. Two traditional compile-time approaches to array bound checking are flow analysis and program verification. This paper presents a new approach, IFV, that integrates flow analysis and program verification techniques. IFV is generally about as effective as program verification yet runs in about the same time as flow analysis. Its typical runtime is proportional to the product of the program size and the number of declared variables. IFV matches loops to templates, which represent commonly occurring loop patterns, to discover loop invariants automatically, which it then uses to strengthen flow analysis. With only seven templates, it handles many common array-access patterns. Patterns not verified by flow analysis are processed with verification techniques entirely automatically. This paper also describes a prototype IFV system that performs compile-time array bound checking for programs in a subset of C. © 1997 John Wiley & Sons, Ltd.     

F@BOOL@: Experiment with a simple verifying compiler based on SAT-solvers

A verifying compiler is computer system program that translates programs written by a human from a high-level language to equivalent executable programs and proves (verifies) mathematical statements specified by a human concerning the properties of the translated programs. The objective of the project F@BOOL@ is to develop a user friendly, compact, and portable verifying compiler of annotated computational programs that uses efficient and reliable automatic SAT solvers as the tools for automatic validation of correctness conditions (instead of semiautomatic proof techniques). In the period from 2006 to 2009, the SAT solver zChaff was used in the project F@BOOL@. The first experiments on the verification of simple Mini-NIL programs were performed using this solver, namely, the programs swapping variable values, checking whether three integer numbers are the sides of an equilateral or an isoscales triangle, and searching for one fake coin among 15 coins using scales. This paper considers the main ideas of the project F@BOOL@ and gives the details of the experiment on the verification of the program solving the coin puzzle.     

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

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

Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects

Current object-oriented approaches to distributed programs may be criticized in several respects. First, method calls are generally synchronous, which leads to much waiting in distributed and unstable networks. Second, the common model of thread concurrency makes reasoning about program behavior very challenging. Models based on concurrent objects communicating by asynchronous method calls, have been proposed to combine object orientation and distribution in a more satisfactory way. In this paper, a high-level language and proof system are developed for such a model, emphasizing simplicity and modularity. In particular, the proof system is used to derive external specifications of observable behavior for objects, encapsulating their state. A simple and compositional proof system is paramount to allow verification of real programs. The proposed proof rules are derived from the Hoare rules of a standard sequential language by a semantic encoding preserving soundness and relative completeness. Thus, the paper demonstrates that these models not only address the first criticism above, but also the second.     

嵌入式DSP系统C语言硬件编程技术

首先介绍了嵌入式DSP系统的基本硬件,然后着重说明用C语言进行硬件编程的好处和基本方法,包括如何调试C语言程序,最后介绍了如何将C语言程序转化为DSP代码.所有内容均基于TI公司的TMS320C55x通用DSP芯片,使用的软件工具是该公司的CCS集成开发环境(IDE).     

mbeddr: instantiating a language workbench in the embedded software domain

Tools can boost software developer productivity, but building custom tools is prohibitively expensive, especially for small organizations. For example, embedded programmers often have to use low-level C with limited IDE support, and integrated into an off-the-shelf tool chain in an ad-hoc way. To address these challenges, we have built mbeddr, an extensible language and IDE for embedded software development based on C. mbeddr is a large-scale instantiation of the Jetbrains MPS language workbench. Exploiting its capabilities for language modularization and composition, projectional editing and multi-stage transformation, mbeddr is an open and modular framework that lets third parties add extensions to C with minimal effort and without invasive changes. End users can combine extensions in programs as needed. To illustrate the approach, in this paper we discuss mbeddr’s support for state machines, components, decision tables, requirements tracing, product line variability and program verification and outline their implementation. We also present our experience with building mbeddr, which shows that relying on language workbenches dramatically reduces the effort of building customized, modular and extensible languages and IDEs to the point where this is affordable by small organizations. Finally, we report on the experience of using mbeddr in a commercial project, which illustrates the benefits to end users.     

Security of Wireless Local Area Networks

The rise of integrated information systems is transforming modern organizations to an extent not envisioned just a few years ago. The dependence of major organizations on these computer supersystems makes it imperative that management provide adequate controls. Many attempts to improve system security are not only inadequate but ill conceived. Our ability to create exceeds our ability to control, and the results can be disastrous. This article discusses the critical role of ID verification in integrated system environments. The inadequacies of memorized passwords as the means of ID verification are discussed, sophisticated ID technologies are described, and the benefits of an integrated approach are enumerated.     

Design and Implementation of the L+C Modeling Language

L-systems are parallel grammars that provide a theoretical foundation for a class of programs used in the simulation of plant development and procedural image synthesis. In particular, the formalism of L-systems guides the construction of declarative languages for specifying input to these programs. We outline key factors that have motivated the development of L-system-based languages in the past, and introduce a new language, L+C, that addresses the shortcomings of its predecessors. We also describe a simulation program, lpfg, which makes it possible to execute models specified in L+C. To this end, L+C programs are translated into C++, compiled into a DLL, and linked with lpfg at runtime. The use of this strategy simplifies the implementation of the modeling system.     

Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language

With the aim of the verification of programs in the C-light language [1], its kernel C-kernel is separated, and an axiomatic semantics for it is suggested. A theorem on soundness of the axiomatic semantics of C-kernel with respect to its operational semantics is proved. The C-light language is used as an input language of the program verification system, which includes a translator to C-kernel and a generator of the correctness conditions for C-kernel programs, which is based on its axiomatic semantics.     

Towards a transformational approach to program verification

Although most typically used in other contexts, program transformations can simplify program verification by transforming a program containing complex language features into a semantically equivalent program containing only simpler language features. The proof of the transformed program can then be performed using a set of proof rules for only the simpler features. There are tradeoffs between the transformational approach and the standard approach to program verification with regard to proof understandability and compactness of programs and assertions, establishing soundness of the program verification method, and providing mechanized support for the method. The transformational approach has clear advantages in some of these aspects. This paper illustrates this transformational approach by considering proof rules for escape statements in iterative constructs, and discusses the tradeoffs with respect to its use. It also suggests how the approach can be applied to other language constructs, including some involving concurrency, and to solving some problems connected with the development of Hoare axiomatizations. Copyright © 1999 John Wiley & Sons, Ltd.