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

9th ifip WG 6.1 international conference on formal methods for open object-based distributed systems, FMOODS 2007

ISBN: (纸本)3540729194

the proceedings contain 19 papers. the topics discussed include: asynchronous session types and progress for object oriented languages;model checking of extended OCL constraints on UML models in SOCLe;analysis of UML activities using dynamic meta modeling;distributed applications implemented in Maude with parameterized skeletons;formal modeling and analysis of the OGDC wireless sensor network algorithm in real-time Maude;adaptation of open component-based systems;a representation-independent behavioral semantics for object-oriented components;a formal language for electronic contracts;a mechanized model of the theory of objects;a refinement method for java programs;refractoring object-oriented specifications with data and processes;a sound and complete shared-variable concurrency model for multi-threaded Java Programs;and performance-oriented comparison of web services via client-specific testing preorders.

关键词： distributed computer systems

来源：评论

学校读者我要写书评

暂无评论

Exploiting the Hierarchical Structure of Rule-based Specifications for Decision Planning

Exploiting the Hierarchical Structure of Rule-Based Specific...

引用

12th Joint international conference on formal methods for open object-based distributed systems/30th international conference on formal Techniques for distributed systems

作者： Boronat, Artur Bruni, Roberto Lafuente, Alberto Lluch Montanari, Ugo Paolillo, Generoso Univ Leicester Dept Comp Sci Leicester LE1 7RH Leics England Univ Pisa Dept Comp Sci I-56100 Pisa Italy IMT Inst Adv Studies Lucca Lucca Italy Lab CINI ITEM Carlo Savy Naples Italy

ISBN: (纸本)9783642134630

Rule-based specifications have been very successful as a declarative approach in many domains, due to the handy yet solid foundations offered by rule-based machineries like term and graph rewriting. Realistic problems, however, call for suitable techniques to guarantee scalability. For instance, many domains exhibit a hierarchical structure that can be exploited conveniently. this is particularly evident for composition associations of models. We propose an explicit representation of such structured models and a methodology that exploits it for the description and analysis of model- and rule-based systems. the approach is presented in the framework of rewriting logic and its efficient implementation in the rewrite engine Maude and is illustrated with a case study.

关键词： Machinery

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：