Zugl.: Bremen, Univ., Diss., 2009

Society is increasingly dependent on the correct operation of concurrent and distributed software systems. Examples of such systems include computer networks, operating systems, telephone switches and flight control systems. Model checking is a useful tool for ensuring the correctness of such systems, because it is a fully automatic technique whose use does not require expert knowledge. Additionally, model checking allows for the production of error trails when a violation of a desired property is detected. Error trails are an invaluable debugging aid, because they provide the programmer with the sequence of events that lead to an error. Model checking typically operates by performing an exhaustive exploration of the state space of the program. Exhaustive state space exploration is not practical for industrial use in the verification of concurrent systems because of the well-known phenomenon of state space explosion caused by the exploration of all possible interleavings of concurrent events. However, the exploration of all possible interleavings is not always necessary for verification. In this dissertation, we show that results from lattice theory can be applied to ameliorate state space explosion due to concurrency, and to produce short error trails when an error is detected. We show that many CTL formulae exhibit lattice-theoretic structure that can be exploited to avoid exploring multiple interleavings of a set of concurrent events. We use this structural information to develop efficient model checking techniques for both implicit (partial order) and explicit (interleaving) models of the state space. For formulae that do not exhibit the required structure, we present a technique called predicate filtering, which uses a weaker property with the desired structural characteristics to obtain a reduced state space which can then be exhaustively explored. We also show that lattice theory can be used to obtain a path of shortest length to an error state, thereby producing short error trails that greatly ease the task of debugging. We provide experimental results from a wide range of examples, showing the effectiveness of our techniques at improving the efficiency of verifying and debugging concurrent and distributed systems. Our implementation is based on the popular model checker SPIN, and we compare our performance against the state-of-the-art state space reduction strategies implemented in SPIN. / text

No description available.

Model Driven Development (MDD) is a paradigm introduced to overcome the complexities of modern software development. In MDD we use models as a primary artifact that is being developed, tested and refined, with code being a result of code generation. Analysis and verification of models is an important aspect of MDD paradigm, because they improve understanding of a developed system and enable discovery of faults early in the development. Even though many analysis methods exist (e.g., model checking, proof systems), they are not directly applicable in the context of industrial MDD tools such as IBM Rational Software Architect Real Time Edition (IBM RSA RTE). One of the main reasons for this inapplicability is the difference between modeling languages used in MDD tools (e.g. UML-RT language in IBM RSA RTE) and languages used in existing tools. These differences require an implementation of a transformation from a modeling language to an input language of a tool. UML-RT as well as other industrial MMD models, cannot be easily translated, if the target languages do not directly support key model features. To address this problem we follow a research direction that deviates from the standard approaches and instead of bringing MDD models to analysis tools, the approach brings analysis "closer" to MDD models. We introduce analysis of UML-RT models dedicated to this modeling language. To this end we use a formal internal representation of UML-RT models that preserves the important features of these models, such as hierarchical structures of components, asynchronous communication and action code. This provides us with formalized models using straightforward transformation. In addition, this approach enables the use of MDD-specific abstractions aiming to reduce the size of the state space necessary. To this end we introduce several MDD-specific types of abstractions for: data (using symbolic execution), structure and behavior. The work also includes model checking algorithms, which use the modular nature of UML-RT models. The proposed approach is implemented in a toolset that enables analysis directly of UML-RT models. We show the results of experiments with UML-RT models developed in-house and obtained from our industrial partner. / Thesis (Ph.D, Computing) -- Queen's University, 2014-06-24 17:58:05.973

A runtime file system checker protects file-system metadata integrity. It checks the consistency of file system update operations before they are committed to disk, thus preventing corrupted updates from reaching the disk. In this thesis, we describe our experiences with building Brunch, a runtime checker for an emerging Linux file system called Btrfs. Btrfs supports many modern file-system features that pose challenges in designing a robust checker. We find that the runtime consistency checks need to be expressed clearly so that they can be reasoned about and implemented reliably, and thus we propose writing the checks declaratively. This approach reduces the complexity of the checks, ensures their independence, and helps identify the correct abstractions in the checker. It also shows how the checker can be designed to handle arbitrary file system corruption. Our results show that runtime consistency checking is still viable for complex, modern file systems.

Pipelined circuits operate as an assembly line that starts processing new instructions while older ones continue execution. Control properties specify the correct behaviour of the pipeline with respect to how it handles the concurrency between instructions. Control properties stand out as one of the most challenging aspects of pipelined circuit verification. Their verification depends on the datapath and memories, which in practice account for the largest part of the state space of the circuit. To alleviate the state explosion problem, abstraction of memories and datapath becomes mandatory. This thesis provides a methodology for an efficient abstraction of the datapath under all possible control-visible behaviours. For verification of control properties, the abstracted datapath is then substituted in place of the original one and the control circuitry is left unchanged. With respect to control properties, the abstraction is shown conservative by both language containment and simulation. For verification of control properties, the pipeline datapath is represented by a network of registers, unrestricted combinational datapath blocks and muxes. The values flowing through the datapath are called parcels. The control is the state machine that steers the parcels through the network. As parcels travel through the pipeline, they undergo transformations through the datapath blocks. The control- visible results of these transformations fan-out into control variables which in turn influence the next stage the parcels are transferred to by the control. The semantics of the datapath is formalized as a labelled transition system called a parcel automaton. Parcel automata capture the set of all control visible paths through the pipeline and are derived without the need of reachability analysis of the original pipeline. Datapath abstraction is defined using familiar concepts such as language containment or simulation. We have proved results that show that datapath abstraction leads to pipeline abstraction. Our approach has been incorporated into a practical algorithm that yields directly the abstract parcel automaton, bypassing the construction of the concrete parcel automaton. The algorithm uses a SAT solver to generate incrementally all possible control visible behaviours of the pipeline datapath. Our largest case study is a 32-bit two-wide superscalar OpenRISC microprocessor written in VHDL, where it reduced the size of the implementation from 35k gates to 2k gates in less than 10 minutes while using less than 52MB of memory.

Telecommunication systems are structured to enable incremental growth, so that new telecommunication features can be added to the set of existing features. With the addition of more features, certain existing features may exhibit unpredictable behaviour. This is known as the feature interaction problem, and it is very old problem in telecommunication systems. Jackson and Zave have proposed a technology, Distributed Feature Composition (DFC) to manage the feature interaction problem. DFC is a pipe-and-filter-like architecture where features are "filters" and communication channels connecting features are "pipes". DFC does not prescribe how features are specified or programmed. Instead, Zave and Jackson have developed BoxTalk, a call-abstraction, domain-specific, high-level programming language for programming features. BoxTalk is based on the DFC protocol and it uses macros to combine common sequences of read and write actions, thus simplifying the details of the DFC protocol in feature models. BoxTalk features must adhere to the DFC protocol in order to be plugged into a DFC architecture (i.e., features must be "DFC compliant"). We want to use model checking to check whether a feature is DFC compliant. We express DFC compliance using a set of properties expressed as linear temporal logic formulas. To use the model checker SPIN, BoxTalk features must be translated into Promela. Our automatic verification process comprises three steps: 1. Explicate BoxTalk features by expanding macros and introducing implicit details. 2. Mechanically translate explicated BoxTalk features into Promela models. 3. Verify the Promela models of features using the SPIN model checker. We present a case study of BoxTalk features, describing the original features and how they are explicated and translated into Promela by our software, and how they are proven to be DFC compliant.

Pinus radiata D. Don is an economically important plantation species to New Zealand that is susceptible to the wood quality flaw 'intra-ring checking'. Intra-ring checking is a term used to describe radial fractures that can occur in the earlywood portion of a growth ring, altering the appearance and resilience of the wood, thereby decreasing its economic value. This thesis presents a study that was part of a broad, ongoing collaborative investigation directed at understanding wood quality issues, with the long term goal of enhancement of future radiata pine crops. These investigations are funded by the Wood Quality Initiative Ltd., and involve basic science, field trials and engineering studies related to intra-ring checking. Specifically, the present study was designed to establish the effects of the mineral nutrients boron, calcium and magnesium on wood formation, to determine whether they are associated with intra-ring checking. This research was carried out in three stages. Firstly, the ultra-structural and biochemical properties of wood with intra-ring checking were examined to determine if specific features of the cell wall were associated with the incidence of intra-ring checks. Electron microscopy techniques revealed that the CML/S1 region of the cell wall often showed a decrease in CML lignin staining and S1 striations in wood with intra-ring checks. However, Klason and acetyl bromide assays did not show a change in lignin content. In order to understand how changes in the CML/S1 region of the cell wall may occur, methods were required that would allow for the observation of wood formation in a controlled environment. In the second stage of this study, an organ culture technique was successfully developed to allow for the growth of radiata pine cambial tissue, sandwiched between phloem and xylem, on a defined nutrient medium. This nutrient medium was manipulated, using ion-binding resins, to control the amount of boron, calcium and magnesium available to the growing tissues, to determine if variations in wood formation could be induced. In the final stage of this research, an extensive comparative examination of different techniques that could be used for the observation and measurement of selected wood properties was undertaken, in order to determine the efficacy of the organ cultures to study wood formation in an altered nutrient environment. Wood properties were examined for various stages of xylogenesis, beginning with cell division and expansion, followed by cell wall deposition, and lastly with the onset of lignification in order to define the success of the culture technique. Electron microscopy investigations suggested that in the presence of very little boron the CML/S1 wall showed darker striation deposits, while an increase in calcium availability, resulted in a more defined CML/S1/S2 wall region compared to the controls. Further examination of the cell walls suggested that pectin esterification and possibly lignification could also be increased by limited boron availability. However, in many of the observed and measured parameters of wood properties, a great deal of complex 'between-tree' and 'within-culture' variation was observed. The results show that elucidation of the association between nutrient availability and the incidence of intra-ring checking can not be established from this organ culture study. In a concurrent study, the preliminary investigation of arabinogalactan-proteins (AGPs) in radiata pine was undertaken. Radiata pine AGPs were positioned in the compound middle lamella of xylem cells, suggesting potential roles in cell-cell adhesion or cell-cell signalling. For the first time, radiata pine AGPs were isolated and characterized in terms of their protein and carbohydrate composition, both of which yielded features typical of AGPs in other plant species. Unique to radiata pine AGPs was the presence of a large proportion of 5-linked arabinose. While the precise function(s) of AGPs are unknown, the results obtained in this research have established a basis for further investigation into the potential for their involvement in wood formation. Overall, new tools have been established to facilitate future research on radiata pine, a commercially important species, and novel results have been obtained concerning the mechanisms of wood formation therein.

Doctor of Philosophy / Steam reconditioning to recover collapse, in mid to low density eucalypt species, has been known for over ninety years. The current industrial practices for steam reconditioning have largely been based on a few older studies, which were often poorly documented and based on very small sample sizes. On top of this, many local practices and ‘rules of thumb’ have developed over time, many of which have a questionable scientific basis. This thesis was undertaken to more rigorously investigate and fundamentally understand collapse recovery, and try to optimise its application. The most obvious variable that kiln operators have control over is the moisture content of the timber prior to steam reconditioning. Experiments were undertaken to generate a range of moisture gradients (ranging from minimal to more industrially realistic) to evaluate the effect of moisture content on collapse recovery. An optimal moisture content for the core of the boards was found to be between about 18–20%, although there was no statistical difference in recoveries between about 17–25% moisture content. Below 15% moisture content recovery dropped off severely and intra-ring internal checking closure was incomplete, while at 25% moisture content an increased level of normal shrinkage, due to the early removal of drying stresses, was the main drawback. Above a core moisture content of about 35% incomplete closure of intra-ring internal checks was again observed. There was little evidence of re-collapse occurring in these high moisture content samples. Previously established relationships between density and collapse and drying rate were again generally observed in these experiments. However, for the first time an effect of collapse in reducing the fitted drying diffusion coefficients was also observed. It was also observed that, provided the moisture content of the board was in the critical range, most of the collapse recovery was achieved in the time it took to get the core of the board up to the steaming temperature of close to 100°C. This suggests that for most thicknesses a conservative reconditioning period of two hours at temperature is all that is required. This recommended shortening of the reconditioning cycle could dramatically increase the throughput of timber through the steam reconditioning chambers. Alternatively, it could mean that where modern final drying kilns are being used, the reconditioning treatment could be carried out within the final drying kiln. A finite element model was developed to demonstrate the mechanism by which collapse recovery occurs. The theory tested was that the elastic component that stores the energy to restore the shape of the deformed cell is primarily found in the S1 and S3 layers. In contrast, the inelastic component is primarily found in the S2 layer. The model generated here provided limited support for this theory.

Zugl.: Chemnitz, Techn. Univ., Diss., 2006