检索结果-内蒙古大学图书馆

2005 International Conference on Foundations of Computer Science, FCS'05

作者： Smith, Marc L. Computer Science Department Colby College Waterville ME 04901-8858 United States

ISBN: (纸本)9781932415711

In unifying theories of programming [1] (UToP), Hoare and He identify the challenge of unification as a goal for computer science, much as the quest for unified theories exist in other scientific disciplines (e.g., physics). UToP presents work begun to unify theories of programming that exist across different programming paradigms, at different levels of abstraction, and described by a variety of presentation styles. In their present state, these differences make it difficult to directly compare one theory to another. Thus, one benefit of unification will be a better understanding of existing separate theories. Hoare and He get the process started in UToP, but much work remains, and the authors identify a great number of remaining challenges. This paper takes up one of those challenges, that of drawing true concurrency into UToP. To do so, we begin with Communicating Sequential Processes [2], an existing theory within UToP, and consider a new notion of lazy observation as a bridge to View-centric Reasoning (VCR), a model for true concurrency.

关键词： True concurrency unifying theories of programming

来源：评论

学校读者我要写书评

暂无评论

APPLYING unifying theories of programming TO REAL-TIME programming

引用

JOURNAL OF INTEGRATED DESIGN & PROCESS SCIENCE 2006年第4期10卷 69-88页

作者： Arenas, Alvaro E. Bicarregui, Juan C. E Sci Ctr CCLRC Rutherford Appleton Lab Chilton Oxon England

This paper introduces an approach to verify the correctness of the implementation of real-time languages. We apply the techniques presented in Hoare and He's "unifying theories of programming" to reason about the correctness of compilers and schedulers for real-time languages, using high-level abstractions such as algebraic laws. In the compilation process, the existence of unique fixed-points is exploited to verify the implementation of crucial real-time operators such as asynchronous input, delay and timeout. It is developed an abstract model for scheduling real-time programs into a uniprocessor machine. The applicability of the model is shown by instancing it with two types of schedulers: a round-robin scheduler, employed when the participating parallel processes do not include deadline constraints, and a priority-based scheduler, used when each participating process is periodic and possesses an associated deadline.

关键词： unifying theories of programming real-time programming compiler specification scheduling

来源：评论

学校读者我要写书评

暂无评论

Semantic inheritance in unifying theories of programming

引用

FORMAL ASPECTS OF COMPUTING 2013年第1期25卷 89-106页

作者： Chen, Yifeng Univ Durham Dept Comp Sci Durham DH1 3LE England

This paper introduces a number of new techniques that support systematic manipulation of predicates, operators, healthiness conditions, laws and fixpoints of recursive programs. Necessary restrictions are imposed on the definition of each model so that the inheritance relation can be established by checking a few conditions on the healthiness conditions and the commands. In particular, we intend to identify the conditions that simplify the closure proof of the program operators and enable laws and fixpoints of a model to be inherited by its submodel without re-proof. A recursive program may correspond to different recursive functions in a model and its submodels, because the primitives such as abort and assignment statements are normally represented as different predicates in different models (although the original definition of each operator is unchanged). This paper studies meta-theory in this more general setting. A fixpoint theorem is discovered and applied to clarify the relationship between the partially correct relational model and the totally correct sequential model in UTP. It is shown that, although assignment statements are modified by the new healthiness conditions in the latter model, most laws (including many that are re-proved in UTP) and fixpoints can be inherited directly without re-proof, if the first argument of every sequential composition in each command tree corresponds to a terminating computation. This result also singles out a small number of laws and fixpoints that may no longer hold in the totally correct model.

关键词： Predicative semantics unifying theories of programming Inheritance Healthiness conditions Fixpoint theory

来源：评论

学校读者我要写书评

暂无评论

unifying semantic foundations for automated verification tools in Isabelle/UTP

引用

SCIENCE OF COMPUTER programming 2020年 197卷 102510-102510页

作者： Foster, Simon Baxter, James Cavalcanti, Ana Woodcock, Jim Zeyda, Frank Univ York Dept Comp Sci Deramore Lane York YO10 5GH N Yorkshire England

The growing complexity and diversity of models used for engineering dependable systems implies that a variety of formal methods, across differing abstractions, paradigms, and presentations, must be integrated. Such an integration requires unified semantic foundations for the various notations, and co-ordination of a variety of automated verification tools. The contribution of this paper is Isabelle/UTP, an implementation of Hoare and He's unifying theories of programming, a framework for unification of formal semantics. Isabelle/UTP permits the mechanisation of computational theories for diverse paradigms, and their use in constructing formalised semantics. These can be further applied in the development of verification tools, harnessing Isabelle's proof automation facilities. Several layers of mathematical foundations are developed, including lenses to model variables and state spaces as algebraic objects, alphabetised predicates and relations to model programs, algebraic and axiomatic semantics, proof tools for Hoare logic and refinement calculus, and UTP theories to encode computational paradigms. (C) 2020 Elsevier B.V. All rights reserved.

关键词： Theorem proving Lenses unifying theories of programming Hoare logic Isabelle/HOL

来源：评论

学校读者我要写书评

暂无评论

unifying theories of reactive design contracts

引用

THEORETICAL COMPUTER SCIENCE 2020年 802卷 105-140页

作者： Foster, Simon Cavalcanti, Ana Canham, Samuel Woodcock, Jim Zeyda, Frank Univ York Dept Comp Sci York YO10 5GH N Yorkshire England

Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying theory for reactive design contracts that provides the basis for modelling and verification of reactive systems. We provide a language for expression and composition of contracts that is supported by a rich calculational theory. In contrast with other semantic models in the literature, our theory of contracts allows us to specify both the evolution of state variables and the permissible interactions with the environment. Moreover, our model of interaction is abstract, and supports, for instance, discrete time, continuous time, and hybrid computational models. Being based in unifying theories of programming (UTP), our theory can be composed with further computational theories to support semantics for multi-paradigm languages. Practical reasoning support is provided via our proof framework, Isabelle/UTP, including a proof tactic that reduces a conjecture about a reactive program to three predicates, symbolically characterising its assumptions and guarantees about intermediate and final observations. This allows us to verify programs with a large or infinite state space. Our work advances the state-of-the-art in semantics for reactive languages, description of their contractual specifications, and compositional verification. (C) 2019 Elsevier B.V. All rights reserved.

关键词： Design-by-contract Reactive systems Automated proof Denotational semantics unifying theories of programming Compositional verification

来源：评论

学校读者我要写书评

暂无评论

Mutation testing in UTP

引用

FORMAL ASPECTS OF COMPUTING 2009年第1-2期21卷 33-64页

作者： Aichernig, Bernhard K. He Jifeng Graz Univ Technol Inst Software Technol A-8010 Graz Austria United Nations Univ Int Inst Software Technol Macau Peoples R China E China Normal Univ Shanghai 200062 Peoples R China

This paper presents a theory of testing that integrates into Hoare and He's unifying Theory of programming (UTP). We give test cases a denotational semantics by viewing them as specification predicates. This reformulation of test cases allows for relating test cases via refinement to specifications and programs. Having such a refinement order that integrates test cases, we develop a testing theory for fault-based testing. Fault-based testing uses test data designed to demonstrate the absence of a set of pre-specified faults. A well-known fault-based technique is mutation testing. In mutation testing, first, faults are injected into a program by altering (mutating) its source code. Then, test cases that can detect these errors are designed. The assumption is that other faults will be caught, too. In this paper, we apply the mutation technique to both, specifications and programs. Using our theory of testing, two new test case generation laws for detecting injected (anticipated) faults are presented: one is based on the semantic level of UTP design predicates, the other on the algebraic properties of a small programming language.

关键词： Specification-based testing Fault-based testing Mutation testing unifying theories of programming Refinement calculus Algebra of programming

来源：评论

学校读者我要写书评

暂无评论

Normal design algebra

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2010年第2期79卷 144-173页

作者： Guttmann, Walter Moeller, Bernhard Univ Augsburg Inst Informat D-86135 Augsburg Germany Univ Ulm Inst Programmiermethod & Compilerbau D-89069 Ulm Germany

We generalise the designs of the unifying theories of programming (UTP) by defining them as matrices over semirings with ideals. This clarifies the algebraic structure of designs and considerably simplifies reasoning about them, for example, since they form a Kleene and omega algebra and a test semiring. We apply our framework to investigate symmetric linear recursion and its relation to tail-recursion. This substantially involves Kleene and omega algebra as well as additional algebraic formulations of determinacy, invariants, domain, pre-image, convergence and Noetherity. Due to the uncovered algebraic structure of UTP designs, all our general results also directly apply to UTP. (C) 2009 Elsevier Inc. All rights reserved.

关键词： unifying theories of programming Semantics Semiring Kleene algebra Omega algebra Fixpoint Linear recursion

来源：评论

学校读者我要写书评

暂无评论

A process algebraic framework for specification and validation of real-time systems

引用

FORMAL ASPECTS OF COMPUTING 2010年第2期22卷 153-191页

作者： Sherif, Adnan Cavalcanti, Ana He Jifeng Sampaio, Augusto Univ York Dept Comp Sci York YO10 5DD N Yorkshire England Univ Fed Pernambuco Ctr Informat Recife PE Brazil E China Normal Univ Inst Software Engn Shanghai 200062 Peoples R China

Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language;its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory.

关键词： Relational models unifying theories of programming CSP Galois connections

来源：评论

学校读者我要写书评

暂无评论

CSP is a retract of CCS

引用

THEORETICAL COMPUTER SCIENCE 2010年第11-13期411卷 1311-1337页

作者： He Jifeng Hoare, Tony Microsoft Res Ltd Cambridge CB3 0FB England E China Normal Univ SEI Shanghai 200062 Peoples R China

Automata theory provides two ways of defining an automaton: either by its transition system, defining its states and events, or by its language, the set of sequences (traces) of events in which it can engage. For many classes of automaton, these forms of definition have been proved equivalent. For example, there is a well-known isomorphism between regular languages and finite deterministic automata. This paper suggests that for (demonically) the non-deterministic automata (as treated in process algebra), the appropriate link between transition systems and languages may be a retraction rather than an isomorphism. A pair of automata, defined in the tradition of CCS by their transition systems, may be compared by a pre-ordering based on some kind of simulation or bisimulation, for example, weak, strong, or barbed. Automata defined in the tradition of CSP are naturally ordered by set inclusion of their languages (often called refinement): variations in ordering arise from different choices of basic event, including for example, refusals and divergences. In both cases, we characterise a theory by its underlying transition system and its choice of ordering. Our treatment is therefore wholly semantic, independent of the syntax and definition of operators of the calculus. We put forward a series of retractions relating the above-mentioned versions of CSP to their corresponding CCS transition models. A retraction is an injection that is (with respect to the chosen ordering) monotonic, increasing and idempotent (up to equivalence). It maps the nodes of a transition system of its source theory to those of a system that has been saturated by additional transitions. Each retraction will be defined by a transition rule, in the style of operational semantics;the proofs use the familiar technique of co-induction, often abbreviated by encoding in the relational calculus. The aim of this paper is to contribute to unification of theories of reactive system programming. More practical

关键词： unifying theories of programming Process algebra CCS CSP Retraction

来源：评论

学校读者我要写书评

暂无评论

On integrating confidentiality and functionality in a formal method

引用

FORMAL ASPECTS OF COMPUTING 2014年第5期26卷 963-992页

作者： Banks, Michael J. Jacob, Jeremy L. Univ York Dept Comp Sci York YO10 5GH N Yorkshire England Altran UK Bath BA1 1AN Avon England

This paper proposes a formal method, based on Circus, for developing software systems that respect a joint specification of functionality and confidentiality attributes. We extend the semantics of Circus to capture the information that users can infer about a system's behaviour, enabling confidentiality and functionality attributes of a system to be specified together. We represent inconsistencies between functionality and confidentiality properties as miracles, rendering insecure functionality infeasible. We present techniques for verifying that a system design's functionality and confidentiality attributes are mutually consistent, and for ensuring that consistency is maintained by refinement steps.

关键词： Information flow security Confidentiality properties Circus unifying theories of programming Miracles Confidentiality-preserving refinement

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：