Maintaining distributed logic programs incrementally

Distributed logic programming languages, which allow both facts and programs to be distributed among different nodes in a network, have been recently proposed and used to declaratively program a wide-range of distributed systems, such as network protocols and multi-agent systems. However, the distributed nature of the underlying systems poses serious challenges to developing efficient and correct algorithms for evaluating these programs. This paper proposes an efficient asynchronous algorithm to compute incrementally the changes to the states in response to insertions and deletions of base facts. Our algorithm is formally proven to be correct in the presence of message reordering in the system. To our knowledge, this is the first formal proof of correctness for such an algorithm.     

Expressiveness and language choice

Specialized languages are often more appropriate than general languages for expressing certain information. However, specialized languages must be chosen carefully because they do not allow all sets of facts to be stated. This paper considers the problems associated with choosing among specialized languages. Methods are presented for determining that a set of facts is expressible in a language, for identifying when additional facts are stated accidentally, and for choosing among languages that can express a set of facts. This research is being used to build a system that automatically chooses an appropriate graphical language to present a given set of facts.     

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

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

Constructing and revising formal arguments in requirements engineering

Confidence that a proposed software-based system, once implemented, will be successful in its environment can be given through a formal argument, typically proof in a formal language. Problems with such arguments include the need to account for the relationships between different kinds of model (models of the proposed system, of assumptions concerning its environment, and of the joint properties, or requirements, which the system should achieve with its environment), and the need to revise these models within an exploratory requirements engineering process. This paper investigates the assumption/commitment style of modelling, originally developed for reasoning about interference in concurrent systems, for developing such arguments. The style, using a simple temporal logic, is used to express these models, with an associated compositional reasoning method allowing arguments to be constructed, and revised with minimal re-work of proof. Some conclusions are drawn concerning the benefits of, and problems with, this approach. The approach is illustrated with a meeting-scheduler example.     

Quantum multi-prover interactive proof systems with limited prior entanglement

This paper gives the first formal treatment of a quantum analogue of multi-prover interactive proof systems. It is proved that the class of languages having quantum multi-prover interactive proof systems is necessarily contained in NEXP, under the assumption that provers are allowed to share at most polynomially many prior-entangled qubits. This implies that, in particular, if provers do not share any prior entanglement with each other, the class of languages having quantum multi-prover interactive proof systems is equal to NEXP. Related to these, it is shown that, in the case a prover does not have his private qubits, the class of languages having quantum single-prover interactive proof systems is also equal to NEXP.     

形式化方法概貌

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明：其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.     

Representing model theory in a type-theoretical logical framework

In a broad sense, logic is the field of formal languages for knowledge and truth that have a formal semantics. It tends to be difficult to give a narrower definition because very different kinds of logics exist. One of the most fundamental contrasts is between the different methods of assigning semantics. Here two classes can be distinguished: model theoretical semantics based on a foundation of mathematics such as set theory, and proof theoretical semantics based on an inference system possibly formulated within a type theory.Logical frameworks have been developed to cope with the variety of available logics unifying the underlying ontological notions and providing a meta-theory to reason abstractly about logics. While these have been very successful, they have so far focused on either model or proof theoretical semantics. We contribute to a unified framework by showing how the type/proof theoretical Edinburgh Logical Framework (LF) can be applied to the representation of model theoretical logics.We give a comprehensive formal representation of first-order logic, covering both its proof and its model theoretical semantics as well as its soundness in LF. For the model theory, we have to represent the mathematical foundation itself in LF, and we provide two solutions for that. Firstly, we give a meta-language that is strong enough to represent the model theory while being simple enough to be treated as a fragment of untyped set theory. Secondly, we represent Zermelo-Fraenkel set theory and show how it subsumes our meta-language. Specific models are represented as LF morphisms.All representations are given in and mechanically verified by the Twelf implementation of LF. Moreover, we use the Twelf module system to treat all connectives and quantifiers independently. Thus, individual connectives are available for reuse when representing other logics, and we obtain the first version of a feature library from which logics can be pieced together.Our results and methods are not restricted to first-order logic and scale to a wide variety of logical systems, thus demonstrating the feasibility of comprehensively formalizing large scale representation theorems in a logical framework.     

Bytecode Analysis for Proof Carrying Code

Out of annotated programs proof carrying code systems construct and prove verification conditions that guarantee a given safety policy. The annotations may come from various program analyzers and must not be trusted as they need to be verified. A generic verification condition generator can be utilized such that a combination of annotations is verified incrementally. New annotations may be verified by using previously verified ones as trusted facts. We show how results from a trusted type analyzer may be combined with untrusted interval analysis to automatically verify that bytecode programs do not overflow. All trusted components are formalized and verified in Isabelle/HOL.     

Modeling high assurance agent-based Earthquake Management System using formal techniques

Disaster management systems are complex applications due to their distributed and decentralized nature. Various components execute in parallel with high need of coordination with each other. In such applications, interaction and communication issues are difficult to model and implement. In this paper, we have proposed agent-based Earthquake Management System (EMS) which is modeled and analyzed using formal approach. Traditionally, such systems undergo through various transformations starting from requirement models and specification to analysis, design and implementation. A variety of formal approaches are available to specify systems for analyzing their structure and behavior; however, there are certain limitations in using these techniques due to their expressiveness and behavior requirements. We have adopted combination of Pi-calculus and Pi-ADL formal languages to model EMS from analysis to design. The formal approach helps to enhance reliability and flexibility of the system by reducing the redundant information. It reduces chances of errors by explicitly mentioning working flow of information. Additionally, a prototype application is presented as proof of concept in EMS context. We have also evaluated our formal specification by using ArchWare and ABC tools; also, comparison of prototype application with major existing techniques is highlighted.     

KALA: Kernel aspect language for advanced transactions

Transaction management is a known crosscutting concern. Previous research has been conducted to express this concern as an aspect. However, such work has used general-purpose aspect languages which lack a formal foundation, and most importantly are unable to express advanced models of transaction management. In this paper, we propose a domain-specific aspect language for advanced transaction management, called KALA, that overcomes these limitations. First, KALA is based on a recognized formalism for the domain of advanced transaction management, called ACTA. Second, as a consequence of being based on the ACTA formalism, KALA covers a wide variety of models for transaction management. Finally, being a domain-specific aspect language, KALA allows programmers to express their needs at a higher level of abstraction than what is achieved with general-purpose aspect languages. This paper reports on the design of KALA and its implementation over Java, based on the Reflex AOP kernel for domain-specific aspect languages.     

Tools for producing formal specifications: a view of current architectures and future directions

During the last decade, one important contribution towards requirements engineering has been the advent of formal specification languages. They offer a well‐defined notation that can improve consistency and avoid ambiguity in specifications. However, the process of obtaining formal specifications that are consistent with the requirements is itself a difficult activity. Hence, various researchers are developing systems that aid the transition from informal to formal specifications. The kind of problems tackled and the contributions made by these proposed systems are very diverse. This paper brings these studies together to provide a vision for future architectures that aim to aid the transition from informal to formal specifications. The new architecture, which is based on the strengths of existing studies, tackles a number of key issues in requirements engineering such as identifying ambiguities, incompleteness, and reusability. The paper concludes with a discussion of the research problems that need to be addressed in order to realise the proposed architecture.     

The Watson Theorem Prover

Watson is a general-purpose system for formal reasoning. It is an interactive equational higher-order theorem prover. The higher-order logic supported by the prover is distinctive in being type free (it is a safe variant of Quine's NF). Watson allows the development of automated proof strategies, which are represented and stored by the prover in the same way as theorems. The mathematical foundations of the prover and the way these are presented to a user are discussed. The paper also contains discussions of experiences with the prover and relations of the prover to other systems.     

A first-order conditional logic for prototypical properties

An approach for representing knowledge about defaults and prototypical properties is presented. This is accomplished by adding to first-order logic a “variable conditional” operator to express relations between entities and prototypical properties of such entities. Truth conditions for this operator are based on a possible-worlds semantics; a proof theory is provided, and the logic is shown to be sound and complete. Properties of the resultant formal system are argued to correspond to common intuitions concerning defaults and prototypical properties. Moreover the system is argued to provide a more appropriate basis for representing knowledge about such entities than other existing approaches.     

A survey on policy languages in network and security management

Policy-driven management is gaining popularity today, mainly due to the ever-growing scale and complexity of large networked systems. In these systems, policies are usually used to simplify the tasks of the system management, thus making way for further system enlargement. Accordingly, a variety of policy languages are proposed to express intentions of administrators in the policy-driven systems, especially for the network and security management. This paper, therefore, investigates current works, discusses the key issues, and then outlines the future work of policy languages.     

Combining assisted and automated deduction

The quest for proved and reliable software goes through theorem provers, which implement proof search. A main trend of these last ten years has been the combination of assisted and automated deduction. Different approaches to this integration are currently studied focussing on efficiency and/or reliability. A promising research direction is to provide formal systems, programming languages and proof environments that support and integrate the two paradigms of computation and deduction. This revised version was published online in June 2006 with corrections to the Cover Date.     

A complete axiomatic semantics of spawning

Summary In modern imperative languages there are two commonly occurring ways to activate concurrently running tasks,splitting (cobegin...coend) andspawning. The programming language Ada makes use of both forms of task activation. We present a formal system for verifying partial correctness specifications of Ada tasks activated by spawning. The system is based upon a view of tasks as histories of events. We show how the mindset of splitting may be applicable when developing a formal system for reasoning about spawning. The resultant proof system is compositional, and a robust extension of partial correctness proof systems for sequential constructs. A transition model is given for spawning, and the proof system is proven complete in the sense of Cook [10] relative to this model, under certain reasonable assumptions. The specific proof rules given apply to a subset of Ada without real-time and distributed termination. Our approach to task verification applies to other imperative languages besides Ada, and the essential parts of our methodology are applicable to other formal systems besides those based on partial correctness reasoning. Sigurd Meldal is professor of informatics at the University of Bergen. He is interested in techniques and tools based on formal methods for development of concurrent software. His current foci are the investigation of algebraic approaches to nondeterminism, and the participation in the design of a concurrent specification, prototyping and implementation language. The latter supplements formal proof with support for run time control of consistency between concurrent systems as specified and as implemented. Meldal received his cand. real. (1982) and dr. scient. (1986) degrees in informatics from the University of Oslo.This research was supported by a grant from the Norwegian Research Council for Science and the Humanities, by the Defense Advanced Research Projects Agency/Information Systems Technology Office under the office of Naval Research contract N00014-90-J1232, by the Air Force Office of Scientific Research under Grant AFOSR83-0255 and by a Fulbright Scholarship from the US Educational Foundation in Norway     

Language support for model-driven software development

This paper is about language technology for facilitating model-driven software development. We argue that two features are important for this purpose: (a) support for explicit meta-representation of programs as an AST-like structure (AST stands for abstract syntax tree) accessible in a programmatic way before and beyond the compilation, and (b) support for user-defined annotations of program elements. That is, we argue for language platforms organized around a Generalized Annotated AST, or GAAST languages for short. We outline the problems with a model-driven development process based on languages without such a support and show how GAAST language technology addresses these problems.     

Annotated reasoning

The application of deduction in various domains resulted in a variety of different techniques to guide the proof search. Many of these techniques incorporate additional knowledge to restrict or select possible proof steps. As a consequence, usually the underlying calculus has to be modified to keep track of this information during the proof search. In this paper we present a general framework for maintaining additional strategic knowledge within a proof. We introduce a formal notion of annotations attached to the constituents of formulas and illustrate how a generic method of inheriting these annotations can be instantiated for various purposes. This revised version was published online in June 2006 with corrections to the Cover Date.