Proving Temporal Properties of Z Specifications Using Abstraction

This paper presents a systematic approach to proving temporal properties of arbitrary Z specifications. The approach involves (i) transforming the Z specification to an abstract temporal structure (or state transition system), (ii) applying a model checker to the temporal structure, (iii) determining whether the temporal structure is too abstract based on the model checking result and (iv) refining the temporal structure where necessary. The approach is based on existing work from the model checking literature, adapting it to Z.

Formalising behaviour trees with CSP

Behaviour Trees is a novel approach for requirements engineering. It advocates a graphical tree notation that is easy to use and to understand. Individual requirements axe modelled as single trees which later on are integrated into a model of the system as a whole. We develop a formal semantics for a subset of Behaviour Trees using CSP. This work, on one hand, provides tool support for Behaviour Trees. On the other hand, it builds a front-end to a subset of the CSP notation and gives CSP users a new modelling strategy which is well suited to the challenges of requirements engineering.

Viewpoint-based testing of concurrent components

The use of multiple partial viewpoints is recommended for specification. We believe they also can be useful for devising strategies for testing. In this paper, we use Object-Z to formally specify concurrent Java components from viewpoints based on the separation of application and synchronisation concerns inherent in Java monitors. We then use the Test-Template Framework on the Object-Z viewpoints to devise a strategy for testing the components. When combining the test templates for the different viewpoints we focus on the observable behaviour of the application to systematically derive a practical testing strategy. The Producer-Consumer and Readers-Writers problems are considered as case studies.

An automated failure mode and effect analysis based on high-level design specificication with behavior trees

Formal methods have significant benefits for developing safety critical systems, in that they allow for correctness proofs, model checking safety and liveness properties, deadlock checking, etc. However, formal methods do not scale very well and demand specialist skills, when developing real-world systems. For these reasons, development and analysis of large-scale safety critical systems will require effective integration of formal and informal methods. In this paper, we use such an integrative approach to automate Failure Modes and Effects Analysis (FMEA), a widely used system safety analysis technique, using a high-level graphical modelling notation (Behavior Trees) and model checking. We inject component failure modes into the Behavior Trees and translate the resulting Behavior Trees to SAL code. This enables us to model check if the system in the presence of these faults satisfies its safety properties, specified by temporal logic formulas. The benefit of this process is tool support that automates the tedious and error-prone aspects of FMEA.

An FPGA network architecture for accelerating 3DES - CBC

This paper presents a DES/3DES core that will support cipher block chaining (CBC) and also has a built in keygen that together take up about 10% of the resources in a Xilinx Virtex II 1000-4. The core will achieve up to 200Mbit/s of encryption or decryption. Also presented is a network architecture that will allow these CBC capable 3DES cores to perform their processing in parallel.

Organic microcavity light-emitting diodes with metal mirrors: dependence of the emission wavelength on the viewing angle

Organic microcavity light-emitting diodes typically exhibit a blueshift of the emitting wavelength with increasing viewing angle. We have modeled the shift of the resonance wavelength for several metal mirrors. Eight metals (Al, Ag, Cr, Ti, Au, Ni, Pt, and Cu) have been considered as top or bottom mirrors, depending on their work functions. The model fully takes into account the dependence of the phase change that occurs on reflection on angle and wavelength for both s and p polarization, as well as on dispersion in the organic layers. Different contributions to the emission wavelength shift are discussed. The influence of the thickness of the bottom mirror and of the choice and thickness of the organic materials inside the cavity has been investigated. Based on the results obtained, guidelines for a choice of materials to reduce blueshift; are given. (C) 2002 Optical Society of America.

Design of microchannel free-space optical interconnects based on vertical-cavity surface-emitting laser arrays

We investigate the design of free-space optical interconnects (FSOIs) based on arrays of vertical-cavity surface-emitting lasers (VCSELs), microlenses, and photodetectors. We explain the effect of the modal structure of a multimodeVCSEL beam on the performance of a FSOI with microchannel architecture. A Gaussian-beam diffraction model is used in combination with the experimentally obtained spectrally resolved VCSEL beam profiles to determine the optical channel crosstalk and the signal-to-noise ratio (SNR) in the system. The dependence of the SNR on the feature parameters of a FSOI is investigated. We found that the presence of higher-order modes reduces the SNR and the maximum feasible interconnect distance. We also found that the positioning of a VCSEL array relative to the transmitter microlens has a significant impact on the SNR and the maximum feasible interconnect distance. Our analysis shows that the departure from the traditional confocal system yields several advantages including the extended interconnect distance and/or improved SNR. The results show that FSOIs based on multimode VCSELs can be efficiently utilized in both chip-level and board-level interconnects. (C) 2002 Optical Society of America.

Behavioral Types for Embedded Software - A Survey

At present, there is a variety of formalisms for modeling and analyzing the communication behavior of components. Due to a tremendous increase in size and complexity of embedded systems accompanied by shorter time to market cycles and cost reduction, so called behavioral type systems become more and more important. This chapter presents an overview and a taxonomy of behavioral types. The intentions of this taxonomy are to provide a guidance for software engineers and to form the basis for future research.

Specification and Evaluation of Safety Properties in a Component-Based Software Engineering Process

Over the past years, component-based software engineering has become an established paradigm in the area of complex software intensive systems. However, many techniques for analyzing these systems for critical properties currently do not make use of the component orientation. In particular, safety analysis of component-based systems is an open field of research. In this chapter we investigate the problems arising and define a set of requirements that apply when adapting the analysis of safety properties to a component-based software engineering process. Based on these requirements some important component-oriented safety evaluation approaches are examined and compared.