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

A shared-variable concurrency analysis of multi-threaded object-oriented programs

thEORETICAL COMPUTER SCIENCE 2009年第2-3期410卷 128-141页

作者： de Boer, F. S. Ctr Math & Comp Sci Amsterdam Netherlands Leiden Inst Adv Comp Sci Leiden Netherlands

In this paper a proof Outline logic is introduced for the partial correctness of multi-threaded object-oriented programs like in Java. the main contribution is a generalization of the Owicki & Gries proof method for shared-variable concurrency to dynamic thread creation. this paper also provides a formal justification of this generalization in terms of soundness and completeness proofs. (C) 2008 Elsevier B.V. All rights reserved.

关键词： Verification Partial correctness Multi-threaded object-oriented programs interference Soundness Completeness

来源：评论

学校读者我要写书评

暂无评论

System Model-based Definition of Modeling Language Semantics

System Model-Based Definition of Modeling Language Semantics

引用

29th ifip formal Techniques for Networked and distributed systems/11th ifip international conference on formal methods for open object-based distributed systems

作者： Groenniger, Hans Ringert, Jan Oliver Rumpe, Bernhard Rhein Westfal TH Aachen Lehrstuhl Informat Softwaretech 3 Aachen Germany

ISBN: (纸本)9783642021374

In this paper, we present an approach to define the semantics for object-oriented modeling languages. One important property of this semantics is to support underspecified and incomplete models. To this end, semantics is given as predicates over elements of the semantic domain. this domain is called the system model which is a general declarative characterization of object systems. the system model is very detailed since it captures various relevant structural, behavioral, and interaction aspects. this allows us to re-use the system model as a. domain for various kinds of object-oriented modeling languages. As a major consequence, the integration of language semantics is straight-forward. the whole approach is supported by tools that do not constrain the semantics definition's expressiveness and flexibility while making it machine-checkable.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

Scala Actors: Unifying thread-based and event-based programming

引用

thEORETICAL COMPUTER SCIENCE 2009年第2-3期410卷 202-220页

作者： Haller, Philipp Odersky, Martin Ecole Polytech Fed Lausanne CH-1015 Lausanne Switzerland

there is an impedance mismatch between message-passing concurrency and virtual machines, such as the JVM. VMs usually map their threads to heavyweight OS processes. Without a lightweight process abstraction, users are often forced to write parts of concurrent applications in an event-driven style which obscures control flow,and increases the burden on the programmer. In this paper we show how thread-based and event-based programming can be unified under a single actor abstraction. Using advanced abstraction mechanisms of the Scala programming language, we implement our approach on unmodified JVMs. Our programming model integrates well with the threading model of the underlying VM. (C) 2008 Elsevier B.V. All rights reserved.

关键词： Concurrent programming Actors threads Events

来源：评论

学校读者我要写书评

暂无评论

Typing Component-based Communication systems

Typing Component-Based Communication Systems

引用

29th ifip formal Techniques for Networked and distributed systems/11th ifip international conference on formal methods for open object-based distributed systems

作者： Lienhardt, Michael Mezzina, Claudio Antares Schmitt, Alan Stefani, Jean-Bernard INRIA France

ISBN: (纸本)9783642021374

Building complex component-based software systems, for instance communication systems based on the Click, Coyote, Appia, or Dream frameworks, call lead to subtle assemblage errors. We present a novel type system and type inference algorithm that prevent interconnection and message-handling errors when assembling component-based communication systems. these errors are typically not captured by classical type systems of host programming languages such as Java or ML. have implemented our approach by extending the description language (ADL) toolset. used by the Dream framework, and used it to check Dream-based communication systems.

关键词： Errors

来源：评论

学校读者我要写书评

暂无评论

formal techniques for distributed systems: Joint 11th ifip WG 6.1 international conference FMOODS 2009 and 29th ifip WG 6.1 international conference FORTE 2009 lisboa, portugal, june 9-12, 2009 proceedings

Formal techniques for distributed systems: Joint 11th IFIP W...

引用

ifip international conference on formal Techniques for distributed systems joint with 11th ifip WG 6.1 international conference on formal methods for open object-based distributed systems, FMOODS 2009 and 29th ifip WG 6.1 international conference on formal Techniques for Networked and distributed systems, FORTE 2009

作者： Lee, David Lopes, Antónia Poetzsch-Heffter, Arnd The Ohio State University 395 Dreese Laboratories Department of Computer Science and Engineering 2015 Neil Avenue ColumbusOH United States University of Lisbon Department of Informatics Campo Grande Lisboa Portugal Technische Universität Kaiserslautern Fachbereich Informatik Gebäude 34 Gottlieb-Daimler-Straße Kaiserslautern Germany

来源：评论

学校读者我要写书评

暂无评论

Amalgamating sessions and methods in object-oriented languages with generics

引用

thEORETICAL COMPUTER SCIENCE 2009年第2-3期410卷 142-167页

作者： Capecchi, Sara Coppo, Mario Dezani-Ciancaglini, Mariangiola Drossopoulou, Sophia Giachino, Elena Univ Turin Dipartimento Informat I-10124 Turin Italy Univ London Imperial Coll Sci Technol & Med Dept Comp London SW7 2AZ England

We suggest an amalgamation of communication-based programming (centered on sessions) and object-oriented programming, whereby sessions between concurrent threads are amalgamated with methods. In our proposal, threads consist of the execution of session bodies on objects and communicate with each other by asynchronously sending/receiving objects on channels. the response to a session request is based on the name of the request and the class of the object receiving the request. the decision of how to continue a session is based on the class of the object sent/received. Sessions can be delegated to other sessions, although sessions themselves are not first class objects. We demonstrate our ideas through a core language with generic types, SAM(9), and an example. We then formalize a small calculus, FSAM(9), and prove subject reduction and progress. the latter property is notoriously difficult to achieve in concurrent calculi. (C) 2008 Elsevier B.V. All rights reserved.

关键词： Session types Foundations of object-oriented programming Subject reduction Progress

来源：评论

学校读者我要写书评

暂无评论

On Process-Algebraic Proof methods for Fault Tolerant distributed systems

On Process-Algebraic Proof Methods for Fault Tolerant Distri...

引用

29th ifip formal Techniques for Networked and distributed systems/11th ifip international conference on formal methods for open object-based distributed systems

作者： Kuhnrich, Morten Nestmann, Uwe Aalborg Univ Dept CS Aalborg Denmark Berlin Inst Technol Sch EECS Berlin Germany

ISBN: (纸本)9783642021374

distributed Algorithms are hard to prove correct. In settings with process failures, things, get worse. Among the proof methods proposed in this context, WO focus On process calculi, which offer a tight connection of proof concepts to the actual code representing the algorithm. We use distributed Consensus as a. case study to evaluate recent developments in this field. Along the way, we find that the classical assertional style for proofs oil distributed algorithms can be used to structure bisimulation relations. For this, we propose the definition of uniform syntactic descriptions of reachable states, oil which state-based assertions call be conveniently formulated. As a result, we get, the best of both worlds: on the one hand invariant-style representation of proof knowledge;oil the other hand the bisimulation-based formal connection to the code.

关键词： Algebra

来源：评论

学校读者我要写书评

暂无评论

Dynamic Symbolic Execution of distributed Concurrent objects

Dynamic Symbolic Execution of Distributed Concurrent Objects

引用

29th ifip formal Techniques for Networked and distributed systems/11th ifip international conference on formal methods for open object-based distributed systems

作者： Griesmayer, Andreas Aichernig, Bernhard Johnsen, Einar Broch Schlatte, Rudolf International Institute for Software Technology United Nations University (UNU-IIST) Macao S.A.R. China Institute for Software Technology Graz University of Technology Austria Department of Informatics University of Oslo Norway

ISBN: (纸本)9783642021374

this, paper extends dynamic symbolic execution to distributed mid concurrent systems. Dynamic symbolic execution is used to systematically identify equivalence classes of input, values and has been shown to scale well to large systems. Although mainly;applied to sequential programs, this scalability makes, it interesting to consider the technique, in the distributed and concurrent setting as well. In order to extend the technique to collcurrent systems: it is necessary to obtain sufficient control over the scheduling of concurrent, activities to avoid race conditions. Creol, a modeling language for distributed concurrent objects, solves this problem by abstracting from a particular scheduling policy but explicity defining scheduling points. this provides sufficient, control to apply the technique of dynamic symbolic of interleaved processes. the technique has been formalized in rewriting logic and executes in Mande.

关键词： Modeling languages

来源：评论

学校读者我要写书评

暂无评论

A Type Graph Model for Java Programs

A Type Graph Model for Java Programs

引用

29th ifip formal Techniques for Networked and distributed systems/11th ifip international conference on formal methods for open object-based distributed systems

作者： Rensink, Arend Zambon, Eduardo Univ Twente Formal Methods & Tools Grp EWI INF NL-7500 AE Enschede Netherlands

ISBN: (纸本)9783642021374

In this work we present a type graph that models all executable construct's of the Java programming language. Such a model is useful for any, graph-based technique that, relies oil a representation of Java programs as graphs. the model can be regarded as a common representation to which to all Java syntax graphs must adhere. We also present the systematic approach that is being taken to generate syntax graphs front Java code. Since the type graph model is comprehensive. i.e., covers the whole language specification, the technique is guaranteed to generate a corresponding graph for any valid Java program. In particular, we want to extract such syntax graphs in order to perform static analysis and model checking of programs written ill Java. Although we focus oil Java, this same approach could be adapted for other programming languages.

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

Reactors: A data-oriented synchronous/asynchronous programming model for distributed applications

引用

thEORETICAL COMPUTER SCIENCE 2009年第2-3期410卷 168-201页

作者： Field, John Marinescu, Maria-Cristina Stefansen, Christian IBM Res Corp TJ Watson Res Ctr Hawthorne NY 10532 USA Univ Copenhagen DIKU Copenhagen O Denmark

Our aim is to define the kernel of a simple and uniform programming model-the reactor model-which can serve as a foundation for building and evolving internet-scale programs. Such programs are characterized by collections of loosely-coupled distributed components that are assembled on the fly to produce a composite application. A reactor consists of two principal components: mutable state, in the form of a fixed collection of relations, and code, in the form of a fixed collection of rules in the style of Datalog. A reactor's code is executed in response to an external stimulus, which takes the form of an attempted update to the reactor's state. As in classical process calculi, the reactor model accommodates collections of distributed, concurrently executing processes. However, unlike classical process calculi, our observable behaviors are sequences of states, rather than sequences of messages. Similarly, the interface to a reactor is simply its state, rather than a collection of message channels, ports, or methods. One novel feature of our model is the ability to compose behaviors both synchronously and asynchronously. Also, our use of Datalog-style rules allows aspect-like composition of separately-specified functional concerns in a natural way. (C) 2008 Elsevier B.V. All rights reserved.

关键词： Reactors Datalog Actors Synchronous programming Asynchronous programming Synchronization distributed programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：