functional languages have been the backbone of Galois' business for the past eight years. they have been very good for us, but not without their own share of challenges. In this talk, we shall stand back and exami...
详细信息
the LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed lambda-calculus. In this methodology, the syntactic and deductiv...
详细信息
the LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed lambda-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms of associated LF types;an encoding is correct (adequote) if and only if it defines a compositional bijection between the apparatus of the deductive system and the associated canonical forms. Given an adequate encoding, one may establish metatheoretic properties of a deductive system by reasoning about the associated LF representation. the Twelf implementation of the LF logical framework is a convenient and powerful tool for putting this methodology into practice. Twelf supports boththe representation of a deductive system and the mechanical verification of proofs of metatheorems about it. the purpose of this article is to provide an up-to-date overview of the LF lambda-calculus, the LF methodology for adequate representation, and the Twelf methodology for mechanizing metatheory. We begin by defining a variant of the original LF language, called Canonical LF, in which only canonical forms (long beta eta-normal forms) are permitted. this variant is parameterized by a subordination relation, which enables modular reasoning about LF representations. We then give an adequate representation of a simply typed lambda-calculus in Canonical LF, both to illustrate adequacy and to serve as an object of analysis. Using this representation, we formalize and verify the proofs of some metatheoretic results, including preservation, determinacy, and strengthening. Each example illustrates a significant aspect of using LF and Twelf for formalized metatheory.
An extended practice in the realm of Software Engineering and programming in industry is the application of coding rules. Coding rules are customarily used to constrain the use (or abuse) of certain programming langua...
详细信息
this paper presents a method that facilitates formal reasoning about the correctness of programs. In this method, properties of programs (e.g. pre- and postconditions of functions) are described in terms of type invar...
详细信息
the goal of operating system (OS) discovery is to learn which OS is running on a distant computer. there are two main strategies for OS discovery: active and passive. Each of them has advantages as well as drawbacks. ...
详细信息
ISBN:
(纸本)1424407982
the goal of operating system (OS) discovery is to learn which OS is running on a distant computer. there are two main strategies for OS discovery: active and passive. Each of them has advantages as well as drawbacks. this paper discusses how answer set programming, a new logicprogramming paradigm, can be used to address, in a simple and elegant way, the problem of operating system discovery in computer networks by logically specifying the problem and providing solutions through automated reasoning. As a result of using such a knowledge representation framework, it is possible to unify the active and the passive methods to OS discovery in a single hybrid approach that has the advantages of both strategies while being much more versatile. Moreover, this paper presents a proof of concept prototype for hybrid operating system discovery.
Tabled evaluation has been proved an effective method to improve several aspects of goal-oriented query evaluation, including termination and complexity. Several "native" implementations of tabled evaluation...
详细信息
We propose a new, minimal specification for real-time Java for safety critical applications. the intention is to provide a profile that supports programming of applications that can be validated against safety critica...
详细信息
We propose a new, minimal specification for real-time Java for safety critical applications. the intention is to provide a profile that supports programming of applications that can be validated against safety critical standards such as DO-178B (1992). the proposed profile is in line withthe Java specification request JSR-302: Safety Critical Java Technology, which is still under discussion. In contrast to the current direction of the expert group for the JSR-302 we do not subset the rather complex Real-Time Specification for Java (RTSJ). Nevertheless, our profile can be implemented on top of an RTSJ compliant JVM
Most of the network service management systems rely on informal specifications, hard-coded programming and relational databases to store and manage network services. As a result, such systems may not be correct facing...
详细信息
ISBN:
(纸本)1424407982
Most of the network service management systems rely on informal specifications, hard-coded programming and relational databases to store and manage network services. As a result, such systems may not be correct facing their requirements and they may not be flexible enough to perform network service management efficiently. this paper presents ongoing work toward an innovative approach, based on knowledge representation, to formally specify the contractual, administrative and technical contents of service level agreements, and the network service management processes and their orchestration promoting network service autonomic management and configuration. By using a knowledge based formal framework and an inference engine capable of reasoning over concepts, relations and changes of state, it is possible to create a more flexible and robust ground for specifying and implementing autonomic and adaptive management tasks.
Despite its widespread use, concurrent programming is still plagued by reliability problems, such as race conditions and deadlock, not found in sequential programs. We present a concurrency framework to help developer...
详细信息
Despite its widespread use, concurrent programming is still plagued by reliability problems, such as race conditions and deadlock, not found in sequential programs. We present a concurrency framework to help developers avoid these error conditions, and make it possible to verify their absence through static analysis.
this work presents a proposal to use aspect orientation in the analysis and design of distributed embedded real-time systems (DERTS). these systems have several requirements directly related to their main characterist...
详细信息
this work presents a proposal to use aspect orientation in the analysis and design of distributed embedded real-time systems (DERTS). these systems have several requirements directly related to their main characteristics, the so-called non-functional requirements (NFR), which refer to orthogonal properties, conditions, and restrictions that are spread out over the entire system. Pure object-oriented methods do not address successfully those so called cross-cutting concerns, so new technologies, like aspect orientation, are applied in order to fulfill this gap. the paper presents DERAF i stributed embedded real-time aspects framework, an extensible and high-level framework (i.e. implementation-independent) to handle NFR of DERTS at earlier design stages. DERAF combines the use of aspects with RT-UML, aiming to separate the handling of non-functional from functional requirements in the model driven design of DERTS. the paper presents the use of DERAF on a case study of an unmanned air vehicle (UAV)
暂无评论