The proceedings contain 15 papers. The topics discussed include: assume-guarantee testing;a specification language for coordinated objects;component-interaction automata as a verification-oriented component-based syst...
ISBN:
(纸本)1595933719
The proceedings contain 15 papers. The topics discussed include: assume-guarantee testing;a specification language for coordinated objects;component-interaction automata as a verification-oriented component-based system specification;performance modeling and prediction of enterprise javabeans with layered queuing network templates;classboxes - an experiment in modeling compositional abstractions using explicit contexts;a specification-based approach to reasoning about pointers;and specification and verification of inter-component constraints in CTL.
The concept of interface in Ada 2005 significantly facilitates its usage as the basis for a software components technology. This technology, taking benefit of the resources that Ada offers for real-time systems develo...
详细信息
ISBN:
(纸本)9783540686217
The concept of interface in Ada 2005 significantly facilitates its usage as the basis for a software components technology. This technology, taking benefit of the resources that Ada offers for real-time systems development, would be suitable for component-based real-time applications that run on embedded platforms with limited resources. This paper proposes a model based technology for the implementation of distributed real-time component-based applications with Ada 2005. The proposed technology uses the specification of components and the framework defined in the LwCCM standard, modifying it with some key features that make the temporal behaviour of the applications executed on it, predictable, and analysable with schedulability analysis tools. Among these features, the dependency on CORBA is replaced by specialized communication components called connectors, the threads required by the components are created and managed by the environment, and interception mechanisms are placed to control their scheduling parameters in a per-transaction basis. This effort aims to lead to a new IDL to Ada mapping, a prospective standard of the OMG.
Access control of sensitive resources is a widely used means to achieve information security. When building large-scale systemsbased on popular commercial component middleware, such as J2EE, a usual way to enforce ac...
详细信息
ISBN:
(纸本)9780769533124
Access control of sensitive resources is a widely used means to achieve information security. When building large-scale systemsbased on popular commercial component middleware, such as J2EE, a usual way to enforce access control is to define access control configurations for components in a declarative manner. These configurations can be interpreted by the J2EE security service to grant or deny access requests to components. However, it is difficult for the developers to define correct access control configurations according to complex and sometimes ambiguous real-world access control requirements. The difficulties come from mainly the complexity of configuring voluminous component methods in large-scale componentbasedsystems and some quality constraints on the configurations, for example, the completeness, consistency and performance overhead of configurations. In this paper, we propose a requirements model driven approach for automatic generation of J2EE access control configurations and demonstrate the approach in a J2EE blueprint application.
The proceedings contain 13 papers. The topics discussed include: performance analysis based upon complete profiles;performance modeling of a JavaEE component application using layered;early detection of JML specificat...
详细信息
ISBN:
(纸本)159593586X
The proceedings contain 13 papers. The topics discussed include: performance analysis based upon complete profiles;performance modeling of a JavaEE component application using layered;early detection of JML specification errors using ESC/Java2;experiments in the use of-simulations for the components-verification of real-time systems;JML-basedverification of liveness properties on a class in isolation;using resemblance to support component reuse and evolution;simplifying reasoning about objects with Tako;specifying java iterators with JML and Esc/Java2;iterator specification with typestates;reasoning about iterators with separation logic;and automatic data environment construction for static device drivers analysis.
A method for formal specification of iterators, which can be used to verify both clients and implementations, is illustrated with a Set abstraction as the underlying collection. Copyright 2006 ACM.
ISBN:
(纸本)159593586X
A method for formal specification of iterators, which can be used to verify both clients and implementations, is illustrated with a Set abstraction as the underlying collection. Copyright 2006 ACM.
Java iterators are notoriously hard to specify. This paper applies a general typestate specification technique that supports several forms of aliasing to the iterator problem. The presented specification conservativel...
详细信息
ISBN:
(纸本)159593586X
Java iterators are notoriously hard to specify. This paper applies a general typestate specification technique that supports several forms of aliasing to the iterator problem. The presented specification conservatively captures iterator protocols and consistency rules. Two limitations of the specification are discussed. Copyright 2006 ACM.
Nowadays component technologies are an integral part of any enterprise production environment. Performance and scalability are among the key properties of such systems. Using Layered Queuing Networks (LQN), one can pr...
详细信息
ISBN:
(纸本)159593586X
Nowadays component technologies are an integral part of any enterprise production environment. Performance and scalability are among the key properties of such systems. Using Layered Queuing Networks (LQN), one can predict the performance of a componentbased system from its design. This work revises the approach of using LQN templates, and offers a case study by using the revised approach to model a realistic component application. Copyright 2006 ACM.
This paper proposes a way to verify temporal properties of a Java class in an extension of JML (Java Modeling Language) called JTPL (Java Temporal Pattern Language). We particularly address the verification of livenes...
详细信息
ISBN:
(纸本)159593586X
This paper proposes a way to verify temporal properties of a Java class in an extension of JML (Java Modeling Language) called JTPL (Java Temporal Pattern Language). We particularly address the verification of liveness properties by automatically translating the temporal properties into JML annotations for this class. This automatic translation is implemented in a tool called JAG (JML Annotation Generator). Correctness of the generated annotations ensures that the temporal property is established for the executions of the class in isolation. Copyright 2006 ACM.
暂无评论