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

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2013年第7期39卷 917-929页

作者： Brandt, Jens Gemuende, Mike Schneider, Klaus Shukla, Sandeep K. Talpin, Jean-Pierre Univ Kaiserslautern Dept Comp Sci D-67653 Kaiserslautern Germany Virginia Tech Arlington Res Ctr Hume Ctr Natl Secur & Technol Arlington VA 22203 USA IRISA INRIA Rennes INRIA Rennes Bretagne Atlantique F-35042 Rennes France

This paper presents an embedding of polychronous programs into synchronous ones. Due to this embedding, it is not only possible to deepen the understanding of these different models of computation, but, more importantly, it is possible to transfer compilation techniques that were developed for synchronous programs to polychronous programs. This transfer is nontrivial because the underlying paradigms differ more than their names suggest: Since synchronous systems react deterministically to given inputs in discrete steps, they are typically used to describe reactive systems with a totally ordered notion of time. In contrast, polychronous system models entail a partially ordered notion of time, and are most suited to interface a system with an asynchronous environment by specifying input/output constraints from which a deterministic controller may eventually be refined and synthesized. As particular examples for the mentioned cross fertilization, we show how a simulator and a verification backend for synchronous programs can be made available to polychronous specifications, which is a first step toward integrating heterogeneous models of computation.

关键词： Model-driven embedded software synchronous programming polychronous programming programming models synchrony hypothesis synchronous guarded commands

来源：评论

学校读者我要写书评

暂无评论

Encapsulation and behavioral inheritance in a synchronous model of computation for embedded system services adaptation

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2005年第2期63卷 241-269页

作者： Kerboeuf, ML Talpin, JP Inst Rech Informat & Syst Aleatoires F-35042 Rennes France

Because it encourages the incremental development of software and the reuse of code by abstracting away implementation details, object orientation is an intuitive and sensible way to conceive large software out of existing application components and libraries. In practice, however, object-orientation is most of the time applied and used with sequentiality in mind. This practice may sometimes be conceptually inadequate for, e.g., control-dominated reactive system components. We address this issue by proposing a process calculus that melts the paradigm of synchronous programming to key object-oriented features: encapsulation and behavioral inheritance with overriding by means of specific algebraic concurrency combinators. This framework provides support for the reuse of components and, more specifically, for the adaptation of embedded systems with new services. Cast in the context of a strict interpretation of the synchronous hypothesis, the proposed model supports a static interpretation of inheritance: overriding is resolved at compile-time (or link-time) and inheritance combinators are translated into primitive synchronous ones. This compilation technique puts object-orientation to work in a syntax-oriented model of synchronous concurrency that naturally supports the incremental, refinement-based design of concurrent systems starting from encapsulated and reused application components. The benefits of our approach are illustrated by a concrete and practical example: the adaptation of services to a plain old telephone service specification. (c) 2004 Elsevier Inc. All rights reserved.

关键词： synchronous programming process calculi encapsulation reuse and behavioral inheritance

来源：评论

学校读者我要写书评

暂无评论

Resource control for synchronous cooperative threads

引用

THEORETICAL COMPUTER SCIENCE 2006年第2-3期358卷 229-254页

作者： Amadio, Roberto M. Dal Zilio, Silvano Univ Paris 07 PPS UMR CNRS 7126 F-75221 Paris 05 France Lab Informat Fondamentale Marseille Marseille France

We develop new methods to statically bound the resources needed for the execution of systems of concurrent, interactive threads. Our study is concerned with a synchronous model of interaction based on cooperative threads whose execution proceeds in synchronous rounds called instants. Our contribution is a system of compositional static analyses to guarantee that each instant terminates and to bound the size of the values computed by the system as a function of the size of its parameters at the beginning of the instant. Our method generalises an approach designed for first-order functional languages that relies on a combination of standard termination techniques for term rewriting systems and an analysis of the size of the computed values based on the notion of quasi-interpretation. We show that these two methods can be combined to obtain an explicit polynomial bound on the resources needed for the execution of the system during an instant. As a second contribution, we introduce a virtual machine and a related bytecode thus producing a precise description of the resources needed for the execution of a system. In this context, we present a suitable control flow analysis that allows to formulate the static analyses for resource control at bytecode level. (C) 2006 Elsevier B.V. All rights reserved.

关键词： synchronous programming resource bound termination quasi-interpretations virtual machine bytecode verification

来源：评论

学校读者我要写书评

暂无评论

A formal approach to reactive systems software: A telecommunications application in ESTEREL

引用

FORMAL METHODS IN SYSTEM DESIGN 1996年第2期8卷 123-151页

作者： Jagadeesan, LJ Puchol, C VonOlnhausen, JE AT&T BELL LABS SOFTWARE PROD RES DEPTNAPERVILLEIL 60566 UNIV TEXAS DEPT COMP SCIAUSTINTX 78712 AT&T BELL LABS DEPT PLATFORMGLOBAL MAINTENANCE OPERATNAPERVILLEIL 60566

ESTEREL is a formally-defined language designed for programming reactive systems;namely, those that maintain a permanent interaction with their environment. The AT&T 5ESS(R) telephone switching system is an example of a reactive system. We describe an implementation in ESTEREL of one feature of a SESS switch;this implementation has been tested in the SESS switch simulator. Furthermore, it has been formally verified that this implementation satisfies some safety properties stated by SESS software development. Our experience indicates that ESTEREL is suitable for programming industrial-strength reactive systems, and affords significant advantages in software development over more traditional programming languages used in industrial settings.

关键词： reactive systems ESTEREL synchronous programming formal methods software verification telecommunications

来源：评论

学校读者我要写书评

暂无评论

Synchronised Shared Memory and Model Checking

引用

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS 2024年第5期23卷 1-30页

作者： Aguado, Joaquin Duenas, Alejandra Otto Friedrich Univ Bamberg Weberei 5 Bamberg Germany ICN Business Sch CEREFIGE 86 Rue Sergent Blandan Nancy France

In this article, a formal generic framework for defining and reasoning about deterministic concurrency in synchronous systems is implemented in the SPIN model checker. Concretely, the work implements the clock- synchronised shared memory (CSM) theory, which extends synchronous programming with more and higher- level CSM data types. These CSM data types are equipped with a synchronisation policy prescribing how concurrent calls to objects methods must be organised. In a policy constructive system, all methods of every object can be scheduled in a policy-conformant manner without deadlocking. In our framework, synchronous policies get codified as PRoMELA never-claims. In this form, the model checker can search for executions (interleavings) that satisfy the synchronous product of all the never-claims, namely policy-conformant schedules for all the CSM objects. The existence of such policy-conformant schedules verifies that the concurrent synchronous system is deterministic. The approach of this article extends beyond a single semantics since it can handle the synchronous programming model as well as the various forms of the sequentially constructive model found in the literature.

关键词： synchronous programming clock-synchronised shared memory model checking determinism concurrency

来源：评论

学校读者我要写书评

暂无评论

The SL synchronous language, revisited

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2007年第2期70卷 121-150页

作者： Amadio, Roberto M. Univ Paris 07 CNRS UMR 7126 PPS F-75251 Paris 05 France

We revisit the SL synchronous programming model introduced by Boussinot and De Simone (IEEE, Trans. on Soft. Eng., 1996). We discuss an alternative design of the model including thread spawning and recursive definitions and we explore some basic properties of the revised model: determinism, reactivity, CPS translation to a tail recursive form, computational expressivity, and a compositional notion of program equivalence. (c) 2006 Elsevier Inc. All rights reserved.

关键词： synchronous programming determinism reactivity CPS translation expressivity bisimulation

来源：评论

学校读者我要写书评

暂无评论

Model-based programming of intelligent embedded systems and robotic space explorers

引用

PROCEEDINGS OF THE IEEE 2003年第1期91卷 212-237页

作者： Williams, BC Ingham, MD Chung, SH Elliott, PH MIT Space Syst & Artificial Intelligence Labs Cambridge MA 02139 USA

programming complex embedded systems involves reasoning through intricate system interactions along lengthy paths between sensors, actuators, and control processors. This is a challenging, time-consuming, and error-prone process requiring significant interaction between engineers and software programmers. Furthermore, the resulting code generally lacks. modularity and robustness in the presence of failure. Model-based programming addresses these limitations, allowing engineers to program reactive systems by specifying high-level control strategies and by assembling commonsense models of the system hardware and software. In executing a control strategy, model-based executives reason about the models "on the fly, " to track system state, diagnose faults, and perform reconfigurations. This paper develops the Reactive Model-Based programming Language (RMPL) and its executive, called Titan. RMPL provides the features of synchronous, reactive languages, with the added ability of reading and writing to state variables that are hidden within the physical plant being controlled. Titan executes an RMPL program using extensive component-based declarative models of the plant to track states, analyze anomalous situations, and generate novel control sequences. Within its reactive control loop, Titan employs propositional inference to deduce the system's current and desired states, and it employs model-based reactive planning to move the plant from the current to the desired state.

关键词： constraint programming model-based autonomy model-based execution model-based programming model-based reasoning robotic execution synchronous programming

来源：评论

学校读者我要写书评

暂无评论

An implementation of constructive synchronous programs in POLIS

引用

FORMAL METHODS IN SYSTEM DESIGN 2000年第2期17卷 135-161页

作者： Berry, G Sentovich, EM Ecole Mines Paris F-06902 Sophia Antipolis France INRIA F-06902 Sophia Antipolis France Cadence Berkeley Labs Berkeley CA 94704 USA

Design tools for embedded reactive systems commonly use a model of computation that employs both synchronous and asynchronous communication styles. We form a junction between these two with an implementation of synchronous languages and circuits (Esterel) on asynchronous networks (POLIS). We implement fact propagation, the key concept of synchronous constructive semantics, on an asynchronous non-deterministic network: POLIS nodes (CFSMs) save state locally to deduce facts, and the network globally propagates facts between them. The result is a correct implementation of the synchronous input/output behavior of the program. Our model is compositional, and thus permits implementations at various levels of granularity from one CFSM per circuit gate to one CFSM per circuit. This allows one to explore various tradeoffs between synchronous and asynchronous implementations.

关键词： embedded systems synchronous programming finite state machines asynchronous networks

来源：评论

学校读者我要写书评

暂无评论

THE synchronous APPROACH TO REACTIVE AND REAL-TIME SYSTEMS

引用

PROCEEDINGS OF THE IEEE 1991年第9期79卷 1270-1282页

作者： BENVENISTE, A BERRY, G ECOLE MINES SOPHIA ANTIPOLIS CTR MATH APPLF-06565 VALBONNEFRANCE

This special issue is devoted to the synchronous approach to reactive and real-time programming. This introductory paper presents and discusses the application fields and the principles of synchronous programming. The major concern of the synchronous approach is to base synchronous programming languages on mathematical models. This makes it possible to handle compilation, logical correctness proofs, and verifications of real-time programs in a formal way, leading to a clean and precise methodology for design and programming.

关键词： logical correctness proofs mathematical models parallel programming program verification real-time programming real-time systems real-time systems synchronous approach synchronous programming verification

来源：评论

学校读者我要写书评

暂无评论

Performance debugging of Esterel specifications

引用

REAL-TIME SYSTEMS 2012年第5期48卷 570-600页

作者： Ju, Lei Bach Khoa Huynh Roychoudhury, Abhik Chakraborty, Samarjit Shandong Univ Sch Comp Sci & Technol Jinan Shandong Peoples R China Natl Univ Singapore Dept Comp Sci Singapore 117548 Singapore Tech Univ Munich Inst Real Time Comp Syst Munich Germany

synchronous languages like Esterel have been widely adopted for designing reactive systems in safety-critical domains such as avionics. Specifications written in Esterel are based on the underlying "synchrony hypothesis", which needs to be validated when Esterel specifications get compiled to real implementations (such as C code). In this work, we present a model-driven and architecture-aware timing analysis framework for C code generated from Esterel and executed on general-purpose processors. By integrating model-level information into the traditional timing analysis, we can efficiently compute accurate time estimates via systematically eliminating a large number of infeasible paths in the generated code. Experimental results show that with our proposed intermediate representation level infeasible path analysis in the model compilation, we obtain up to 16.1 % tighter WCET estimates compared to the traditional assembly code level infeasible path detection with substantially less analysis time. Furthermore, by maintaining the traceability links between Esterel specifications and the generated C code, we are able to map the time-critical computations at the C-level back to the Esterel-level.

关键词： Esterel synchronous programming Performance debugging WCET analysis

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：