Search

We describe the goals, architecture, design considerations and use of the common aspect proof environment (CAPE). The CAPE is an extensible framework integrating formal methods and analysis tools for aspect-oriented programs. It is intended both to encourage the use of formal methods and analysis tools for systems with aspects and to facilitate the development of new tools for aspect analysis. The general principles of the CAPE are first explained, and the components and their high-level organization are given. The user interfaces are described, providing both application oriented and tool oriented Eclipse views. A description of the tools already integrated into the CAPE is given, and some analysis and verification scenarios are shown for an example aspect system. The aid of the CAPE in tool evaluation and experimentation with innovative usage of tools is demonstrated. As one example, verification aspects are used to aid in the abstraction and specification needed for formal analysis in Java Pathfinder. The scenarios and strategies employed are steps towards a methodology that includes multiple formal methods tools in aspect-oriented software development.

Aspects are program modules that include descriptions of key events (called join-points) and code segments (called advice) to be executed at those key events when the aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness of an aspect relative to its specification, independently of any specific underlying system to which it may be woven, and also allows establishing noninterference among aspects, or detecting potential interference. The specification includes assumptions about properties of the underlying system, and guaranteed properties of any system after the aspect is woven into it. The approach is based on model checking of a state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the join-points, and the state machine of the aspect advice. The tableau of the LTL assumption is used in a unique way, as a representative of any underlying system satisfying the assumptions. This is the first technique for once-and-for-all verification of an aspect relative to its specification, thereby increasing the modularity of proofs for systems with aspects. The individual correctness proofs along with proofs of interference freedom are appropriate for a library of reusable aspects, when multiple aspects are to be woven to a system.

The reasons for translating a description of a model in one notation into another are reviewed. Such model descriptions are used as input to formal verification tools or as design-level descriptions for protocols or hardware. Translations are used to produce input to a different tool to verify properties not verified in the source model, and to connect notations that have no associated verification tool to those that do. The VeriTech framework for translation is described. A system being analyzed is seen as a collection of versions, along with a characterization of how the versions are related, and properties known to be true of each version. The versions are given in different notations connected through a core notation by compilers from and to the notations of existing tools and specification methods. The reasons that translations cannot always be exact are analyzed. To facilitate optimizations during retranslation, error tracing, and analysis, additional information is gathered during translation, and is also included with the system being analyzed. The concept of a faithful relation among models and families of properties true of those models is presented. In this framework families of properties are provided with uniform syntactic transformations, in addition to the translations of the models. This framework generalizes common instances of relations among translations previously treated in an ad hoc way. The example of refinement translations is shown in detail. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation.

Web applications can be classified as hybrids between hypermedia and information systems. They have a relatively simple distributed architecture from the user viewpoint, but a complex dynamic architecture from the designer viewpoint. They need to respond to operation by an unlimited number of heterogeneously skilled users, address security and privacy concerns, access heterogeneous, up-to-date information sources, and exhibit dynamic behaviors that involve such processes as code transferring. Common system development methods can model some of these aspects, but none of them is sufficient to specify the large spectrum of Web application concepts and requirements. This paper introduces OPM/Web, an extension to the Object-Process Methodology (OPM) that satisfies the functional, structural and behavioral Web-based information system requirements. The main extensions of OPM/Web are adding properties of links to express requirements, such as those related to encryption; extending the zooming and unfolding facilities to increase modularity; cleanly separating declarations and instances of code to model code transferring; and adding global data integrity and control constraints to express dependence or temporal relations among (physically) separate modules. We present a case study that helps evaluate OPM/Web and compare it to an extension of the Unified Modeling Language (UML) for the Web application domain.

We show how compact Resource Utilization Models (RUMs) can be extracted from concrete overly-detailed models of systems or sub-systems in order to model energy-aware software. Using the Counterexample-Guided Abstraction Refinement (CEGAR) approach, along with model-checking tools, abstract models can be generated that help establish key properties relating to energy consumption. This approach is illustrated by the concrete example of a network manager sub-system. This work is part of an overall design methodology for energy-aware software.

Events and aspects that respond to them can and should be defined, specified, and verified in a modular way, as an aid in understanding and guaranteeing the correctness of each on its own. However, finding the appropriate interfaces and abstractions and expressing them precisely is not an easy task. Moreover, formally verifying large models is often unfeasible for existing model-checking tools.We present an abstraction refinement scheme to verify aspects and to define and correct both aspect and event specifications. This allows considering smaller models and learning the needed event guarantees at each step. In addition, this technique can be used to find sound abstractions to check event reachability. Moreover, the technique is applied for detecting interference in systems where there are responses to complex events and aspects may be activated within the execution of other aspects.

AspectJ pointcuts relate to a specific execution point in the program and thus AspectJ is not capable of naturally expressing high-level events that are the culmination of a series of more basic events. Yet, there is a real need for expressing such events when dealing with domains having terminology at a level of abstraction higher than the program's code, e.g., software process support, usability evaluation of user interfaces, or detecting illegal banking practices. Here, we present a framework called HighspectJ that provides a structured AspectJ-based solution for defining and utilizing high-level events. The framework treats an event as a first-class object, separates between the identification and the treatment of the event, and facilitates definition of events in layers, where higher level events are defined in terms of lower level ones. In addition, definition and reuse of high-level events using aspects is facilitated by an event repository which contains event building blocks. The framework is described process support is given.

An extended specification for aspects, and a new verification method based on model checking are used to establish the correctness of strongly-invasive aspects, independently of any particular base program to which they may be woven. Such aspects can change the underlying base program variables to new states, and after the aspect advice has completed, the base program code continues from states that were previously unreachable.

An extended specification for aspects, and a new verification method based on model checking are used to establish the correctness of strongly-invasive aspects, independently of any particular base program to which they may be woven. Such aspects can change the underlying base program variables to new states, and after the aspect advice has completed, the base program code continues from states that were previously unreachable. The needed changes in the MAVEN model checker are described, and the soundness of the verification method is proven. An example is shown of its application to aspects that provide various bonus points to student grading programs.

Aspects are program modules that include descriptions of key events (called joinpoints) and code segments (called advice) to be executed at those key events when the aspect is bound (woven) to an underlying system. The MAVEN tool verifies the correctness of an aspect relative to its specification, independently of any specific underlying system to which it may be woven. The specification includes assumptions about properties of the underlying system, and guaranteed properties of any system after the aspect is woven into it. The approach is based on model checking of a single state machine constructed using the linear temporal logic (LTL) description of the assumptions, a description of the joinpoints, and the state machine of the aspect advice. The tableau of the LTL assumption is used in a unique way, as a representative of any underlying system satisfying the assumptions. This is the first technique for once-and-for-all verification of an aspect relative to its specification, thereby increasing the modularity of proofs for systems with aspects.

Special issue on Software Engineering Curriculum Development; International audience; As new software engineering techniques emerge, there's a cognitive shift in how developers approach a problem's analysis and how they design and implement its software-based solution. Future software engineers must be appropriately and effectively trained in new techniques' fundamentals and applications. With techniques becoming more mature, such training moves beyond specialized industrial courses into postgraduate curricula (as advanced topics) and subsequently into undergraduate curricula. A model curriculum for aspect-oriented software development provides guidelines about fundamentals, a common framework, and a step toward developing a body of knowledge.

Usually, aspects enhance a software product by being composed - or woven - into it. Here, on the other hand, we use aspects to support the software development process itself. The underlying system, i.e., the system to which the aspects are woven, is not the software product but the environment where it is developed. We define aspects to support both software process management and software process modeling. As we show, the aspects can monitor, enforce, or even partially implement compliance with desired development practices. They also provide a basis for a precise description of a software development process. As a case-study, we consider Extreme Programming (XP) and the Eclipse platform. XP is a software development methodology described by underlying values, principles and practices. We present examples of AspectJ aspects that support XP guidelines such as "compose tests before coding" or "provide rapid feedback". Their abstract definitions are shown to be platform independent and correspond to the XP ontology. Their concrete implementation and weaving is connected to Eclipse, an open-source development environment. The design and a prototype implementation of aspects for XP over Eclipse is described.

Generic categories of aspects are described, and their potential value is explained. For some categories, broad classes of syntactically identifiable temporal properties, such as safety, liveness, or existence properties, are guaranteed to hold for a system with any aspect of the category woven into it, if the property was true in the system without the aspect. Thus classes of properties preserved by the aspect are defined. Moreover, relatively simple verification techniques are shown to hold for some classes of temporal properties over systems augmented with some other categories of aspects. Verification of new properties added by the aspects is also considered. Each category is defined in terms of the semantic transformation it makes to the state graphs of underlying systems. A generic procedure to identify syntactically when an aspect belongs to a category is described and related to existing code analysis systems that use static code analysis and dataflow techniques. The definitions of categories, identification procedures, and lemmas about property classes provide the needed foundations that justify and motivate automatic code analysis modules to identify aspect categories. The categories enable simpler proofs of correctness than would otherwise be possible, and exploiting their characteristics can aid in software development.

Software systems specifications are often described as a set of typical scenarios. Some of the desired scenarios are crosscut by other requirements, called aspects, also naturally described as scenarios. Aspect descriptions are independent of the description of the non-aspectual scenarios, but the crosscutting relationship between them has to be specified, so for each aspect a description of its join-points is provided. When aspectual scenarios are added to the system, we need to prove that every execution is equivalent to one in which the aspectual scenarios occur as blocks of operations immediately at their join-points, and all the other operations form a sequence of non-aspectual scenarios, interrupted only by the aspectual scenarios. We extend an existing method of automatic verification for non-aspect systems to the case of systems with scenario-based aspect specifications. A prototype implementation based on Cadence SMV is also extended accordingly.

As system complexity has increased, so has interest in reusing software components in early development phases. While most current modeling methods support design of generic parameterized frameworks or patterns and weaving them into specific models, they do not support open reuse, i.e., the ability to develop partially specified components and refine them in the target application. We introduce an open reuse formalism that is based on OPM/Web, an extension of object-process methodology for distributed systems and Web applications. Our open reuse is accomplished by a three-step process, consisting of designing reusable models, creating basic woven models, and enhancing their specification. We model a reusable component through partially specified environmental elements that are bound to concrete counterparts when the component is integrated into the system under development. Rules for modeling and combining components are defined and applied to a Web example.

Support for the incremental design of aspects themselves has been neglected, even as the use of aspects in conjunction with underlying systems is gaining acceptance. The ways in which aspects can cooperate or interfere with each other need to be made explicit at the design level. An aspect architecture, a new software architecture viewtype, is proposed, and its general principles are explained. An instantiation for extending UML is described, where designs of aspects provide maximal flexibility, and a new concern diagram is provided to show how aspects can be combined to treat different concerns of a system. An example shows aspect architecture views of a digital sound recorder.

Specifications that describe typical scenarios of operations have become common for software applications, using, for example, use-cases of UML. For a system to conform with such a specification, every execution sequence must be equivalent to one in which the specified scenarios occur sequentially, where we consider computations to be equivalent if they only differ in that independent operations may occur in a different order.

The reasons for translating a description of a model in one notation into another are reviewed. This includes both translating entire models and describing different aspects of a system using different notations.In order to demonstrate the ideas, the VeriTech framework for translation is described. A system being analyzed is seen as a collection of versions, along with a description of how the versions are related. The versions are given in different notations connected through a core notation by compilers from and to the notations of existing tools and specification methods. The reasons that translations cannot always be exact are analyzed, based on experience with over ten separate compiler translations among formal methods notations. Additional information gathered during translation is described, to facilitate optimizations, error tracing, and analysis.The concept is presented of a faithful relation among models and families of properties true of those models. In this framework families of properties are provided with uniform syntactic transformations, in addition to the translations of the models. This framework is shown appropriate for common instances of relations among translations previously treated in an ad hoc way. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation. Open research directions are suggested concerning faithful transformations, additional information, error tracing, and optimizing translations.

Numerous translations exist between the design notations of formal methods tools, usually between two specific notations. In addition, more general translation frameworks are under development. For any translation it is vital that properties true of the semantic interpretations of the source and the translated notations are closely related. Some possible applications of translations among model descriptions are described and key issues in translating among models with inconsistent features are identified, leading to a source and a target model that do not always preserve the correctness of properties in a simple way. The concept is presented of a faithful relation among models and families of properties true of those models. In this framework families of properties are provided with uniform syntactic transformations, in addition to the translations of the models. Three variants are presented, depending on the intended use of the translation, so that the correctness of a property in a model corresponds to the correctness of the transformed property in the translated model. This framework is shown appropriate for common instances of relations among translations previously treated in an ad hoc way. Furthermore, it allows expressing connections among models where one is neither a refinement nor an abstraction of the other. The classes of properties that can be faithful for a given translation provide a measure of the usefulness of the translation.

We report a case of renal trauma followed by hypertension and spontaneous recovery in a 2-week-old girl involved in a road accident.

Web applications exhibit dynamic behaviour through such features as animation, rapidly changing presentations, and interactive forms. The growing complexity of web applications requires a rigorous modelling approach capable of clearly and explicitly addressing code mobility issues. While mobile agent systems and programming languages support the implementation of code mobility with features such as applets or mobile agents, existing system analysis and design methods lack the facilities to model code mobility satisfactorily. OPM/Web is an extension of object-process methodology (OPM) for modelling distributed systems and web applications that enables intuitive modelling of code mobility concepts in a single framework. We propose generic OPM/Web models for common code mobility design paradigms, including Remote Evaluation, Code-on-Demand, PUSH and Mobile Agents. An OPM/Web model of a mobile application that handles requests for Quality of Service over the internet exemplifies the use and advantages of modelling such systems in OPM/Web.

Surgical sutures are known to potentiate the development of wound infection. The purpose of this study was to investigate whether the capability of bacteria to adhere to various types of sutures has a significant effect on their ability to cause infections. Bacterial adherence to sutures was quantitatively measured using radiolabeled bacteria. In vitro adherence assays revealed remarkable variations in the affinity of bacteria to the various sutures: nylon bound the least bacteria while bacterial adherence to braided sutures (silk, Ti-cron, Dexon) was five to eight folds higher. The degree of infection obtained in mice in the presence of different sutures nicely correlated with their adherence properties. The different removal rate of adherent bacteria (glutaraldehyde-fixed) from various sutures by the tissue factors in mice supports the hypothesis that bacterial adherence to suture materials plays a significant role in the induction of surgical infection. Our observation points out at the need for careful suture selection in contaminated wounds. The adherence properties of sutures should be considered in any future surgical suture design.

The notion of equifairness, strengthening the familiar notion of fairness, is introduced as a scheduling policy of nondeterminism and concurrency. Under this notion, it is infinitely often the case that the number of selections of each of a family of infinitely often jointly enabled processes is equal. A proof rule for proving equifair termination is introduced and proved to be semantically complete.

Partially interpreted program schemas are suggested as a tool for formally specifying and defining the range of applicability of patterns of communication. The body of a schema syntactically resembles a program, but contains free variables which represent uninterpreted program sections, domains, functions, or other aspects of the program. The specification of the schema includes both applicability requirements and result assertions, as well as specifications for the free variables. A schema may be instantiated to obtain a correct program for a problem statement by matching a problem's assumptions and requirements to a schema specification, and appropriately substituting entities from the problem statement for the free variables in both the specification and the body of the schema. Examples are given of the types of schemas and specifications needed for distributed computing, and of the potential variety of instantiations.

A case is presented of ascites infected with Candida in a cirrhotic patient. Candida infection of the ascitic fluid and candidemia were found 24 hours after perforation of a gastric ulcer. Combined intravenous therapy with Amphotericin B and 5-Fluorocytosine eradicated the infection within two weeks. The need for comprehensive therapeutic approach in the debilitated patient prone to fungal and bacterial infection is emphasized.

We have treated 20 patients with multiple injuries and concomitant myocardial contusion. The diagnosis of myocardial contusion was based mainly on serial ECG tracings which showed arrhythmias, dynamic ischaemic patterns or conduction disturbances. The clinical and laboratory findings of cardiac contusion are sometimes indistinguishable from those found in multiple injuries. Furthermore, they are overshadowed by the overt manifestation of cerebral, thoraco-abdominal and skeletal injuries. Awareness and prompt diagnostic measures are essential in the diagnosis of cardiac injury. Strict cardiac monitoring following multiple trauma will prevent serious or even fatal outcome of cardiac injury.

This is the report of the successful surgical treatment of a pancreatic abscess in a 15-month-old girl.