Integration of informal and formal development of object-oriented safety-critical software

The KeY system allows for the integrated informal and formal development of object-oriented Java software. In this paper we report on a major industrial case study involving safety-critical software for the computation of a particular kind of railway timetable used by train conductors. Our case study includes formal specification of requirements both on the analysis and the implementation level. Particular emphasis in our research is placed on the challenge to make authoring and maintenance of formal specifications easier. We demonstrate that the technique of specification patterns as implemented in KeY for the language OCL yields significant improvements.     

E<Emphasis Type="SmallCaps">ssence</Emphasis>: A constraint language for specifying combinatorial problems

Essence is a formal language for specifying combinatorial problems in a manner similar to natural rigorous specifications that use a mixture of natural language and discrete mathematics. Essence provides a high level of abstraction, much of which is the consequence of the provision of decision variables whose values can be combinatorial objects, such as tuples, sets, multisets, relations, partitions and functions. Essence also allows these combinatorial objects to be nested to arbitrary depth, providing for example sets of partitions, sets of sets of partitions, and so forth. Therefore, a problem that requires finding a complex combinatorial object can be specified directly by using a decision variable whose type is precisely that combinatorial object.     

Radl 形式规格说明相对正确性研究

在形式规格说明的获取任务中,一个重要问题是验证获取得到的形式规格说明的正确性.即给定一个问题需求P,往往可以获取多种不同形式的规格说明,如何验证这些不同形式的规格说明均正确?问题需求的非(半)形式化与形式规格说明的形式化两者之间差异的本性,使得该问题成为软件需求工程中一个具有挑战性的问题.提出一种基于形式化推导的方法来验证同一问题不同形式规格说明的相对正确性,通过证明不同形式规格说明与问题需求某个最为直截明了的形式规格说明Si等价来实现,而Si使用PAR方法和PAR平台转换为可执行程序,通过测试已经得到确认.为了支持该方法,进一步提出了扩展的逻辑系统和辅助证明算法.使用Radl语言作为形式规格说明语言,通过排序搜索、组合优化领域的两个典型实例对该方法进行了详细的阐述.实际使用效果表明,该方法不仅能够有效地验证Radl形式规格说明的正确性,还具备良好的可扩充性.该方法在规格说明的正确性验证、算法优化、程序等价性证明等研究领域具有潜在的理论意义与应用价值.     

Systematic incremental validation of reactive systems via sound scenario generalization

Validating the specification of a reactive system, such as a telephone switching system, traffic controller, or automated network service, is difficult, primarily because it is extremely hard even tostate a set of complete and correct requirements, let alone toprove that a specification satisfies them. In the ISAT project[10], end-user requirements are stated as concrete behavior scenarios, and a multi-functional apprentice system aids the human developer in acquiring and maintaining a specification consistent with the scenarios. ISAT's Validation Assistant (isat-va) embodies a novel, systematic, and incremental approach to validation based on the novel technique ofsound scenario generalization, which automatically states and proves validation lemmas. This technique enablesisat-va to organize the validity proof around a novel knowledge structure, thelibrary of generalized fragments, and provides automated progress tracking and semi-automated help in increasing proof coverage. The approach combines the advantages of software testing and automated theorem proving of formal requirements, avoiding most of their shortcomings, while providing unique advantages of its own.     

Semantics,calculi, and analysis for object-oriented specifications

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development.     

Decision problems for lower/upper bound parametric timed automata

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as an upper bound. For such automata, we show that basic decision problems, such as emptiness, finiteness and universality of the set of parameter valuations for which there is a corresponding infinite accepting run of the automaton, is Pspace-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still Pspace-complete, if the lower bound parameters are not compared with the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL\mathsf{MITL} _0,∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are Pspace-complete.     

基于模拟关系的精化检测方法

精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同形式化语言进行建模,如能证明两者间存在某种精化关系且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质, traces、stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,大大提高了算法性能,且该方法能直接用于traces精化检测.在此基础上,本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法.此外,本文还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.     

Automated theorem proving in mathematics

TheMuscadet theorem prover is a knowledge-based system able to prove theorems in some non-trivial mathematical domains. The knowledge bases contain some general deduction strategies based onnatural deduction, mathematical knowledge and metaknowledge. Metarules build new rules, easily usable by the inference engine, from formal definitions. Mathematical knowledge may be general or specific to some particular field.Muscadet proved many theorems in set theory, mappings, relations, topology, geometry, and topological linear spaces. Some of the theorems were rather difficult.Muscadet is now intended to become an assistant for mathematicians in discrete geometry for cellular automata. In order to evaluate the difficulty of such a work, researchers were observed while proving some lemmas, andMuscadet was tested on easy ones. New methods have to be added to the knowledge base, such as reasoning by induction, but also new heuristics for splitting and reasoning by cases. It is also necessary to find good representations for some mathematical objects.     

Facilitating formal specification acquisition by using recursive functions on context-free languages

Although formal specification techniques are very useful in software development, the acquisition of formal specifications is a difficult task. This paper presents the formal specification language LFC, which is designed to facilitate the acquisition and validation of formal specifications. LFC uses context-free languages for syntactic aspect and relies on a new kind of recursive functions, i.e. recursive functions on context-free languages, for semantic aspect of specifications. Construction and validation of LFC specifications are machine-aided. The basic ideas behind LFC, the main aspects of LFC, and the use of LFC and illustrative examples are described.     

Towards Monitoring-Oriented Programming: A Paradigm Combining Specification and Implementation

With the explosion of software size, checking conformance of implementation to specification becomes an increasingly important but also hard problem. Current practice based on ad-hoc testing does not provide correctness guarantees, while highly confident traditional formal methods like model checking and theorem proving are still too expensive to become common practice. In this paper we present a paradigm for combining formal specification with implementation, called monitoring-oriented programming (MoP), providing a light-weighted formal method to check conformance of implementation to specification at runtime. System requirements are expressed using formal specifications given as annotations inserted at various user selected places in programs. Efficient monitoring code using the same target language as the implementation is then automatically generated during a pre-compilation stage. The generated code has the same effect as a logical checking of requirements and can be used in any context, in particular to trigger user defined actions, when requirements are violated. Our proposal is language- and logic- independent, and we argue that it smoothly integrates other interesting system development paradigms, such as design by contract and aspect oriented programming. A prototype has been implemented for Java, which currently supports requirements expressed using past time and future time linear temporal logics, as well as extended regular expressions.     

一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。     

ON A SIMPLE COMBINATORIAL STRUCTURE SUFFICIENT FOR SYBLYING NONTRIVIAL SELF-REPRODUCTION

Abstract

An abstract research on self-reproduction from the viewpoint of systems theory is made, investigating the problem of how simple the combinatorial laws of formal systems can be chosen and to still ensure nontrivial self-reproduction.

We take as a base the heuristic of the theory of cellular automata in the sense of von Neumann. We operate in a formal, microscopic, submolecular world as our patterns of cells shall represent some kind of artificial molecules. Computation- and construction-universal, self-reproducing systems are regarded as artificial living beings according to the common heuristic. A simple combinatorial system M of only four very simple dynamic laws is introduced and it can be shown that even in a world governed by this system M nontrivial self-reproduction can be established, thus illuminating what simple combinatorial structures allow for the handling of such logical somewhat difficult phenomenas as self-organization, self-reproduction, etc.

To receive a model slightly more adapted to nature than the concepts of cellular automata our system M obeys the law of microscopic reversibility, allows concurrent activities, and needs no regulation by a synchronizing device.     

Using integer clocks to verify clock-synchronization protocols

We use the Uppaal model checker for timed automata to verify the Timing-Sync time-synchronization protocol for sensor networks (TPSN), the clock-synchronization algorithm of Lenzen, Locher and Wattenhofer (LLW) for general distributed systems, and the clock-thread technique of the software monitoring with controllable overhead algorithm (SMCO). Clock-synchronization algorithms such as TPSN, LLW, and SMCO must be able to perform arithmetic on clock values to calculate clock drift and network propagation delays. They must also be able to read the value of a local clock and assign it to another local clock. Such operations are not directly supported by the theory of timed automata. To overcome this formal-modeling obstacle, we augment the Uppaal specification language with the integer clock-derived type. Integer clocks, which are essentially integer variables that are periodically incremented by a global pulse generator, greatly facilitate the encoding of the operations required to synchronize clocks as in the TPSN, LLW, and SMCO protocols. With these integer-clock-based models in hand, we use Uppaal to verify a number of key correctness properties, including network-wide time synchronization, bounded clock skew, bounded overhead skew, and absence of deadlock. We also use the Uppaal Tracer tool to illustrate how integer clocks can be used to capture clock drift and resynchronization during protocol execution.     

ConSpec – A Formal Language for Policy Specification

The paper presents ConSpec, an automata based policy specification language. The language trades off clean semantics to language expressiveness; a formal semantics for the language is provided as security automata. ConSpec specifications can be used at different stages of the application lifecycle, rendering possible the formalization of various policy enforcement techniques.     

Use of executable formal specifications in user validation

Requirements validation through feedback with users is of paramount importance in producing a high quality requirements specification document. Use of an executable formal specification offers an effective combination of formalism and pragmatism. This allows not only the systematic development of a concise specification of a system, but it also enables developers to execute the specification to receive feedback at an early stage. Executable formal specification languages have traditionally been used as an effective prototyping tool to facilitate developer validation, that is the developer can, via specification execution either individually or in a peer review format, explore the consequences of the specification. However, their use in requirements validation is often not user orientated, which may in turn reduce the effectiveness of the approach. This paper reports on work to facilitate the user validation process based on executable formal specifications. A user orientated process with a systematic framework can maximise the effectiveness of the user validation process. Dialogue management based on scenarios enables an effective communication between a system and its users. Our approach also enables the intertwining of equational specifications in a modular algebraic specification language and conventional implementations in a modular programming language. This introduces a judicious choice of rigour, techniques and tools to support the user dialogue with a prototype system to effectively and explicitly address the user validation process. © 1998 John Wiley & Sons, Ltd.     

Syntactic reductions for efficient deadlock analysis

A well‐known problem in the verification of concurrent systems based on model checking is state explosion: concurrent systems are often represented by automata with a prohibitive number of states. A reduction technique to reduce state explosion in deadlock checking is presented. The method is based on an automatic syntactic simplification of a calculus of communicating systems (CCS) specification, which keeps the parts of the program structure that may lead to a deadlock and deletes the other parts. Copyright © 2002 John Wiley & Sons, Ltd.     

Before and after vacuity

In formal verification, we verify that a system is correct with respect to a specification. Cases like antecedent failure can make a successful pass of the verification procedure meaningless. Vacuity detection can signal such “meaningless” passes of the specification, and indeed vacuity checks are now a standard component in many commercial model checkers. We address two dimensions of vacuity: the computational effort and the information that is given to the user. As for the first dimension, we present several preliminary vacuity checks that can be done without the design itself, which implies that some information can be found with a significantly smaller effort. As for the second dimension, we present algorithms for deriving two types of information that are not provided by standard vacuity checks, assuming for a model M and formula φ: (a) behaviors that are possibly missing from M (or wrongly restricted by the environment) (b) the largest subset of occurrences of literals in φ that can be replaced with false simultaneously without falsifying φ in M. The complexity of each of these problems is proven. Overall this extra information can lead to tighter specifications and more guidance for finding errors. A preliminary version of this article was published in the proceedings of MEMOCODE 2007 [18].