The proceedings contain 31 papers. The topics discussed include: executable computational logics: combining formal methods and programminglanguage based system design;from use cases to system implementation: statecha...
ISBN:
(纸本)0769519237
The proceedings contain 31 papers. The topics discussed include: executable computational logics: combining formal methods and programminglanguage based system design;from use cases to system implementation: statechart based co-design;goal-oriented requirements analysis for process control systems design;analyzing concurrency in computational networks;finding good counter-examples to aid design verification;high level verification for control intensive systems using predicate abstraction;formal verification of an Intel XScale processor model with scoreboarding, specialized execution pipelines, and imprecise data-memory exceptions;engineering changes in field modifiable architectures;hierarchical and incremental verification for system level design: challenges and accomplishments;and how to compute the refinement relation for parameterized systems.
The hardware description language TDL has been designed with the goal to generate machine-dependent postpass optimizers and analyzers from a concise specification of the target processor. TDL is assembly-oriented and ...
详细信息
ISBN:
(纸本)3540201025
The hardware description language TDL has been designed with the goal to generate machine-dependent postpass optimizers and analyzers from a concise specification of the target processor. TDL is assembly-oriented and provides a generic modeling of irregular hardware constraints that are typical for many embedded processors. The generic modeling supports graph-based and search-based optimization algorithms. An important design goal of TDL was to achieve extendibility, so that TDL can be easily integrated in different target applications. TDL is at the base of the PROPAN system that has been developed as a retargetable framework for high-quality code optimizations at assembly level. For two contemporary microprocessors, the Analog Devices SHARC 2106x, and the Philips TriMedia TM1000, significant improvements of the code produced by production-quality compilers could be achieved with short retargeting time. TDL has also been used for implementing postpass optimizations for the Infineon C16x/ST10 processor that are part of a commercial postpass optimizer. TDL specifications are concise and can be produced in short time.
We compare two different facilities for running cleanup actions for objects that are about to reach the end of their life. Destructors, such as we find in C++, are invoked synchronously when an object goes out of scop...
详细信息
ISBN:
(纸本)9781581136289
We compare two different facilities for running cleanup actions for objects that are about to reach the end of their life. Destructors, such as we find in C++, are invoked synchronously when an object goes out of scope. They make it easier to implement cleanup actions for objects of well-known lifetime, especially in the presence of exceptions. languages like Java[8], Modula-3[12], and C#[6] provide a different kind of "finalization" facility: Cleanup methods may be run when the garbage collector discovers a heap object to be otherwise inaccessible. Unlike C++ destructors, such methods run in a separate thread at some much less well-defined time. We argue that these are fundamentally different, and potentially complementary, language facilities. We also try to resolve some common misunderstandings about finalization in the process. In particular: The asynchronous nature of finalizers is not just an accident of implementation or a shortcoming of tracing collectors;it is necessary for correctness of client code, fundamentally affects how finalizers must be written, and how finalization facilities should be presented to the user. An object may legitimately be finalized while one of its methods are still running. This should and can be addressed by the language specification amd client code.
While Java provides many software engineering benefits, it lacks a coherent module system and instead provides only packages (which are primarily a name space mechanism) and classloaders (which are very low-level). As...
详细信息
While Java provides many software engineering benefits, it lacks a coherent module system and instead provides only packages (which are primarily a name space mechanism) and classloaders (which are very low-level). As a result, large Java applications suffer from unexpected interactions between independent components, require complex CLASSPATH definitions, and are often extremely complex to install and maintain. We have implemented a module system for Java called MJ that is implemented with class loaders, but provides a much higher-level interface. High-level properties can be specified in a module definition and are enforced by the module system as new modules are loaded. To experimentally validate the ability of MJ to properly handle the complex module interrelationships found in large Java server systems, we replaced the classloader mechanisms of Apache Tomcat 4.1.18 [27] with 30 MJ modules. The modified Tomcat is functionally identical to the original, but requires no CLASS PATH definitions, and will operate correctly even if user code loads a different version of a module used by Tomcat, such as the Xerces XML parser [31]. Furthermore, by making a small change to the Java core libraries enabled by MJ, we obtained a 30% performance improvement in a servlet microbenchmark.
As the use of XML is rapidly growing, a growing number of users without programming skills will need to query XML data. Although designed to be easily understood by humans, XQuery, the XML standard query language, has...
详细信息
ISBN:
(纸本)9781581136241
As the use of XML is rapidly growing, a growing number of users without programming skills will need to query XML data. Although designed to be easily understood by humans, XQuery, the XML standard query language, has the typical syntax of programminglanguages, which most users dislike. In this paper we describe a graphical language (XQBE) inspired by "Query By Example" (QBE), a popular relational query language used by MS Access. XQBE covers a significant subset of XQuery and is supported by a prototype enabling the formulation of queries on a graphical interface and their translation into XQuery, thus providing non-trivial querying capabilities to a wide spectrum of users. Simple queries are easily represented in XQBE, but many "complex" queries allow as well for an intuitive graphical representation.
This paper presents the specification of a programminglanguage for implementing the deliberation cycle of cognitive agents. The mental attitudes of cognitive agents are assumed to be represented in an object language...
详细信息
This paper presents the specification of a programminglanguage for implementing the deliberation cycle of cognitive agents. The mental attitudes of cognitive agents are assumed to be represented in an object language. The implementationlanguage for the deliberation cycle is considered as a meta-language the terms of which denote formulae from the object language. Without losing generality, we use the agent programminglanguage 3APL as the object language. Using the meta-deliberation language, one can program the deliberation process of a cognitive agent. We discuss a set of programming constructs that can be used to program various aspects of the deliberation cycle including the planning constructs.
We present an extension of the development method Fusion/UML that translates the results of analysis and design into the formal specification language Object-Z. The extended process establishes a consistency relations...
详细信息
ISBN:
(纸本)0769519237
We present an extension of the development method Fusion/UML that translates the results of analysis and design into the formal specification language Object-Z. The extended process establishes a consistency relationship between analysis and design. Furthermore, a formal specification for the implementation is produced.
In this paper we propose an XML-based markup language, called XSTER, for embodied agents, based on the scripting language STEP. XSTEP is the XML-based successor of STEP The scripting language STEP incorporates the for...
详细信息
ISBN:
(纸本)0769519342
In this paper we propose an XML-based markup language, called XSTER, for embodied agents, based on the scripting language STEP. XSTEP is the XML-based successor of STEP The scripting language STEP incorporates the formal semantics of dynamic logic, and has been implemented in the distributed logic programminglanguage DLP, a tool for the implementation of 3D web agents. In this paper, we discuss the issues of markup languagedesign for embodied agents and several aspects of the implementation and application of XSTEP.
Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. The dynamic semantics of aspects is typically specified by appealing to an u...
详细信息
ISBN:
(纸本)3540405313
Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. The dynamic semantics of aspects is typically specified by appealing to an underlying object-oriented language via a compiler transformation known as weaving. This treatment is unsatisfactory for several reasons. Firstly, this semantics violates basic modularity principles of object-oriented programming. Secondly, the converse translation from object-oriented programs into an aspect language has a simple canonical flavor. Taken together, these observations suggest that aspects are worthy of study as primitive computational abstractions in their own right. In this paper, we describe an aspect calculus and its operational semantics. The calculus is rich enough to encompass many of the features of extant aspect-oriented frameworks that do not involve reflection. The independent description of the dynamic semantics of aspects enables us to specify the correctness of a weaving algorithm. We formalize weaving as a translation from the aspect calculus to a class-based object calculus, and prove its soundness.
作者:
Gomes, LCosta, AUniv Nova Lisboa
Fac Ciencias & Tecnol Dept Elect Engn UNINOVACtr Robot Inteligente P-2825 Monte De Caparica Portugal
This paper proposes a set of procedures addressing the implementation of Statechart models. The main goal of this set of procedures is to lift the structuring mechanisms presented in statecharts to the top level. In t...
详细信息
ISBN:
(纸本)0769518877
This paper proposes a set of procedures addressing the implementation of Statechart models. The main goal of this set of procedures is to lift the structuring mechanisms presented in statecharts to the top level. In this sense, the complexity of statechart implementation will be similar to the complexity of communicating concurrent state machines and the platforms selected to support implementation will not need to have specific capabilities to directly support the structuring mechanisms of Harel's statecharts. The framework is the design of embedded systems (in the sense of reactive real time systems) and automation applications, either industrial automation or building automation, either the emphasis is on system, hardware or software levels, using or not co-design techniques. An application focused on hardware implementation using VHDL as implementationlanguage is used as an example.
暂无评论