Firstly, we extend the Generalised Substitution Language, and therefore the principles of weakest precondition calculus, to embrace differential constraints. Our approach is based on generalising the traditional view that a Generalised Substitution specifies a fragment of a sequential programme. We consider a Generalised Substitution to represent an autonomous transformation which is 'clocked' repeatedly to perform its computation at regular intervals. In the case of such components composed synchronously, we can generalise the notion of weakest precondition to traces (sequences of values) of inputs and outputs. In our approach we characterise traces with first order constraints as 'step' predicates over adjacent elements in the trace. We refer to these as 'acceptance criteria'. We also generalise our calculus to cover nth order differentials. Secondly, we adapt weakest precondition to traces characterised by state machines which represent sequencing constraints. We do this by introducing a form of state machines called 'acceptance machines' which constrain traces of variable values in an alternative way to differential properties. Using the Generalised Substitution Language once more we present a semantics for the propagation of acceptance machines in a manner analagous to predicate transformers. We also use acceptance machines to specify safety properties which have been derived from the safety process. The requirements can then be shown correct with respect to these properties. Finally, we consolidate and integrate our differential calculus and state machine theory with a domain specific formal framework, focusing on the practical application of the theory in a real engineering setting. The domain specific framework which we have selected is Practical Formal Specification. It is a framework which has been developed specifically for use in the engine (and aircraft) control software domain and is based on the decomposition of requirements into components whose usage can be scoped by the specification of environmental and contextual assumptions.

Test data sets have been automatically generated for both numerical and string data types to test the functionality of simple procedures and a good sized UNIX filing system from their Z specifications. Different structured properties of software systems are covered, such as arithmetic expressions, existential and universal quantifiers, set comprehension, union, intersection and difference, etc. A CASE tool ZTEST has been implemented to automatically generate test data sets. Test cases can be derived from the functionality of the Z specifications automatically. The test data sets generated from the test cases check the behaviour of the software systems for both valid and invalid inputs. Test cases are generated for the four boundary values and an intermediate value of the input search domain. For integer input variables, high quality test data sets can be generated on the search domain boundary and on each side of the boundary for both valid and invalid tests. Adaptive methods such as Genetic Algorithms and Simulated Annealing are used to generate test data sets from the test cases. GA is chosen as the default test data generator of ZTEST. Direct assignment is used if it is possible to make ZTEST system more efficient. Z is a formal language that can be used to precisely describe the functionality of computer systems. Therefore, the test data generation method can be used widely for test data generation of software systems. It will be very useful to the systems developed from Z specifications.

In this thesis we investigate some of the issues involved in creating a reversible variant of the formal software development language B. We consider the effects of regarding computation as a potentially reversible process, yielding a number of new programming structures which we integrate into an implementation-level language RB0, a more expressive variant of B0, the current implementation-level language for B. Since reversibility simplifies garbage collection, in RB0 we make use of more abstract, set-based data types, normally available in B only at the specification level. Similarly, we propose extending the domain of abstract functions currently specifiable in B to allow them to become concrete functions, thereby furnishing B with a functional sub-language. We also investigate expanding the use of Lambda calculus from the abstract stage of B to the implementation. Unlike B0, RB0 will not disallow non-determinism, and can also specify what we call Prospective Value computations (which are described). The executable language implements all of these features. After introducing some preliminary concepts, we review the work leading to the rise of Reversible Computing as a possible answer to the growing problem of energy dissipation in modern processors. We describe the language RB0, and demonstrate the use of its features, introducing the companion language RB1 and its role in the process. We then introduce our execution platform, the Reversible Virtual Machine (RVM), and translate some of the examples developed earlier into RVM code. For the concrete functions, we provide a proposed syntax and translation schema to enable consistent translation to RVM, and introduce a postfix Lambda notation to link the RB0 specification to the RVM’s own postfix notation. We provide comprehensive translation schemas for those parts of RB0 which would be found in B operations; these will form the basis of an automated translation engine. In addition, we look at a denotational semantics for Bunch theory, which has proved useful in formalising the underlying concepts.

No description available.

O constante aumento da velocidade de processamento, devido principalmente à utilização de um número cada vez maior de processadores, tem propiciado grandes avanços no projeto e na construção de sistemas computacionais paralelos. Entretanto o desempenho de muitas aplicações é afetado pela latência das operações de Entrada e Saída de dados. Para solucionar esse problema, sistemas de arquivos paralelos, que oferecem acesso paralelo aos dados armazenados em diversos discos, vêm sendo desenvolvidos. O desenvolvimento desses sistemas complexos pode ser beneficiado pela adoção de Técnicas de Descrição Formal (TDFs), durante as fases de projeto e especificação dos mesmos, as quais podem ser aliadas a técnicas de implementação durante as demais fases. Neste sentido, este projeto propõe uma abordagem baseada em frameworks e na TDF Extended State Transition Language (Estelle), para a especificação formal, validação, implementação e teste de sistemas dessa categoria. Um framework conceitual que descreve um sistema funcional é apresentado, e dois estudos de caso são desenvolvidos dando origem a dois sistemas de arquivos derivados do framework. Uma metodologia para a validação, que usa ferramentas de simulação, é apresentada. Um dos estudos de caso é implementado semi-automaticamente, a partir de sua especificação formal Estelle, e comparações de desempenho com o mesmo sistema implementado manualmente são realizadas. / The constant increase of processing speed, mainly due to the use of a large number of processors, has allowed an improvement in the design and building of parallel computation systems. However, the performance of several types of applications is affected by the latency originated from Input/Output operations on data. In order to solve this problem parallel file systems, which allow parallel access to the data stored on a set of discs, have been developed. The design of such complex systems can benefit from the adoption of implementation techniques allied with Formal Description Techniques (FDTs). Aimed to introduce the use of FDTs in the development cycle of distributed parallel file systems, this work proposes an approach, based on framework and the FDT Extended State Transition Language (Estelle), for the formal specification, validation, implementation and testing of systems belonging to this domain. A conceptual framework that describes a basic functional system is presented, and two case studies are developed from it. A methodology for Estelle specification validation that makes use of simulation tools is also proposed in this work. One of the systems, developed as a case study, is semi-automatically implemented from its Estelle formal specification, and performance comparisons with a hand-coded implementation of the same system are done.

O constante aumento da velocidade de processamento, devido principalmente à utilização de um número cada vez maior de processadores, tem propiciado grandes avanços no projeto e na construção de sistemas computacionais paralelos. Entretanto o desempenho de muitas aplicações é afetado pela latência das operações de Entrada e Saída de dados. Para solucionar esse problema, sistemas de arquivos paralelos, que oferecem acesso paralelo aos dados armazenados em diversos discos, vêm sendo desenvolvidos. O desenvolvimento desses sistemas complexos pode ser beneficiado pela adoção de Técnicas de Descrição Formal (TDFs), durante as fases de projeto e especificação dos mesmos, as quais podem ser aliadas a técnicas de implementação durante as demais fases. Neste sentido, este projeto propõe uma abordagem baseada em frameworks e na TDF Extended State Transition Language (Estelle), para a especificação formal, validação, implementação e teste de sistemas dessa categoria. Um framework conceitual que descreve um sistema funcional é apresentado, e dois estudos de caso são desenvolvidos dando origem a dois sistemas de arquivos derivados do framework. Uma metodologia para a validação, que usa ferramentas de simulação, é apresentada. Um dos estudos de caso é implementado semi-automaticamente, a partir de sua especificação formal Estelle, e comparações de desempenho com o mesmo sistema implementado manualmente são realizadas. / The constant increase of processing speed, mainly due to the use of a large number of processors, has allowed an improvement in the design and building of parallel computation systems. However, the performance of several types of applications is affected by the latency originated from Input/Output operations on data. In order to solve this problem parallel file systems, which allow parallel access to the data stored on a set of discs, have been developed. The design of such complex systems can benefit from the adoption of implementation techniques allied with Formal Description Techniques (FDTs). Aimed to introduce the use of FDTs in the development cycle of distributed parallel file systems, this work proposes an approach, based on framework and the FDT Extended State Transition Language (Estelle), for the formal specification, validation, implementation and testing of systems belonging to this domain. A conceptual framework that describes a basic functional system is presented, and two case studies are developed from it. A methodology for Estelle specification validation that makes use of simulation tools is also proposed in this work. One of the systems, developed as a case study, is semi-automatically implemented from its Estelle formal specification, and performance comparisons with a hand-coded implementation of the same system are done.

A specification of a software program, hardware component, or system, is a description of what the system is required to do without describing how it is to be done. Specifications provide the necessary details for system developers, suppliers, users and regulators to understand and agree upon the requirements of a system. It is therefore vital that specifications are clear, concise, complete, and are free of ambiguity and inconsistency. Specifications are usually expressed using a combination of informal natural language descriptions, diagrams, and formal mathematical techniques. The degree to which formal mathematics is used depends on the nature of the application and the criticality of the function being described. In industries where the cost of a system or software failure is high, such as national defence and government, banking, transport, energy, and communication, and some manufacturing industries, formal specification is recommended because it offers greater clarity and consistency, and moreover, formal specification are machine readable, allowing some automated checking to be applied. However, poorly written formal specifications can be less useful than informal specifications if they are unreadable (or not clear), or if they are overly large or complex (or not concise), making it hard to determine whether they are consistent or complete. In particular, if the system itself is large or complex, or it features multiple and diverse aspects of behaviour, it can be difficult to capture all aspects of its behaviour clearly and concisely in a monolithic formal model, or within a single formal notation. In many cases this is because the modeling approach may be particularly suited to some aspects of the system but not to others. The widely accepted solution to this problem is to use diverse modeling techniques to specify the different aspects of the system from different viewpoints. This results in a number of view specifications that taken together make up the complete specification of the system. The thesis introduces structuring mechanisms for the formal specification language Z that allow the view specifications of a system to be described, combined and reused. Specification encapsulation and parameter abstraction and application are explored along with object-oriented concepts such sub-typing and sub-classing. Two case studies, which are based on a language-based editor and a database system, are provided to illustrate how the techniques developed in this thesis may be used.

Orchestrated web service applications are highly distributed applications that accomplish business goals by executing services offered by partners. This dependance on partner services allows the development of more flexible, modular applications. For a classical distributed system, correctness can be ensured by statically checking the composition of the components that make up the system against properties of interest. However, in the case of web service applications, there are various conditions that make this type of analysis insufficient. For example, partners can be dynamically discovered, which means that we cannot create a definitive model of the system to analyze. Web service applications can also display new behaviour at execution time, so statically checked properties of the system may not hold throughout the system's lifetime. Due to these limitations of static analysis, this thesis concentrates on the dynamic analysis of web service applications, specifically, by monitoring runtime events. The goal of runtime monitoring is to check whether an application violates a given specification of its behaviour during its execution. The behaviour of the system can be specified in a number of ways, e.g., as a set of temporal properties, assertions or even scenarios. During execution, application events are intercepted and used to determine if the system is violating its specification. Moreover, monitoring the system as it runs provides a chance to recover from an error once a problem has been detected. This is critical in the domain of web service applications, as bugs are potentially exposed to millions of users before they are found/fixed. We present techniques to address several major challenges facing the creation of an industrial-strength runtime monitoring and recovery framework for web service applications. The first milestone for achieving this goal is the creation of an adequate property specification language. This language must be expressive enough to capture the distributed, interactive, and message-driven nature of web service applications, but must also be amenable to efficient runtime monitoring. We propose Web Sequence Diagrams (W-SD), a language that, we feel, meets these criteria. Specifications expressed in W-SD permit the analysis of orchestrations involving multiple partners, from the point of view of the orchestrating service. The second contribution of this thesis is the creation of an industrial-strength online runtime monitoring and recovery framework that is non-intrusive, supports the dynamic discovery of web services, deals with synchronous and asynchronous communication, as well as partner services implemented in different languages. Developers using this framework can specify and efficiently monitor a variety of temporal behaviour. If recovery is enabled, properties are monitored proactively, so this framework allows developers to effortlessly enable error recovery in applications being monitored. The last contribution of this thesis is the development of recovery plans from runtime errors. Given an application path which led to a failure and a monitor which detected it, we have developed various techniques and optimizations that make recovery plan generation feasible in practice. For some of the violations, such plans essentially involve "going back" -- compensating the occurred actions until an alternative behaviour of the application is possible. For other violations, such plans include both "going back" and "re-planning" -- guiding the application towards a desired behaviour.

Orchestrated web service applications are highly distributed applications that accomplish business goals by executing services offered by partners. This dependance on partner services allows the development of more flexible, modular applications. For a classical distributed system, correctness can be ensured by statically checking the composition of the components that make up the system against properties of interest. However, in the case of web service applications, there are various conditions that make this type of analysis insufficient. For example, partners can be dynamically discovered, which means that we cannot create a definitive model of the system to analyze. Web service applications can also display new behaviour at execution time, so statically checked properties of the system may not hold throughout the system's lifetime. Due to these limitations of static analysis, this thesis concentrates on the dynamic analysis of web service applications, specifically, by monitoring runtime events. The goal of runtime monitoring is to check whether an application violates a given specification of its behaviour during its execution. The behaviour of the system can be specified in a number of ways, e.g., as a set of temporal properties, assertions or even scenarios. During execution, application events are intercepted and used to determine if the system is violating its specification. Moreover, monitoring the system as it runs provides a chance to recover from an error once a problem has been detected. This is critical in the domain of web service applications, as bugs are potentially exposed to millions of users before they are found/fixed. We present techniques to address several major challenges facing the creation of an industrial-strength runtime monitoring and recovery framework for web service applications. The first milestone for achieving this goal is the creation of an adequate property specification language. This language must be expressive enough to capture the distributed, interactive, and message-driven nature of web service applications, but must also be amenable to efficient runtime monitoring. We propose Web Sequence Diagrams (W-SD), a language that, we feel, meets these criteria. Specifications expressed in W-SD permit the analysis of orchestrations involving multiple partners, from the point of view of the orchestrating service. The second contribution of this thesis is the creation of an industrial-strength online runtime monitoring and recovery framework that is non-intrusive, supports the dynamic discovery of web services, deals with synchronous and asynchronous communication, as well as partner services implemented in different languages. Developers using this framework can specify and efficiently monitor a variety of temporal behaviour. If recovery is enabled, properties are monitored proactively, so this framework allows developers to effortlessly enable error recovery in applications being monitored. The last contribution of this thesis is the development of recovery plans from runtime errors. Given an application path which led to a failure and a monitor which detected it, we have developed various techniques and optimizations that make recovery plan generation feasible in practice. For some of the violations, such plans essentially involve "going back" -- compensating the occurred actions until an alternative behaviour of the application is possible. For other violations, such plans include both "going back" and "re-planning" -- guiding the application towards a desired behaviour.

Šiame magistriniame darbe yra aptariama logistikos svarba prekybinėse įmonėse. Atliekamas sandėliavimo ir transportavimo, bei efektyvaus klientų užsakymų tenkinimo naudojant informacines technologijas optimizavimo tyrimas. Panašių programų analizė. Neformaliai ir formaliai Z kalba sandėlių sistemos aprašymas. Bendro prekybos centro ir sandėlio PLA modelio parengimas su agregacine schema ir koncepciniu modeliu, formalia specifikacija. Taip pat išskirtos perėjimų ir išėjimų operacijos. Vėliau bendrojo PLA modelio pritaikymas sandėlių ir prekybos centrų logistikos schemai, agregacinės schemos paruošimas. Formaliųjų Z ir PLA metodų apjungimas kuriant imitacinius modelius, bei imitacinio modelio paruošimas ir jo analizė. Z ir PLA matodų pranašumai ir trūkumai kuriant imitacinius modelius. Išvadose darbo pasiekti rezultatai. / In this graduate work is consideration about logistic importance in commercial companies. Optimization analysis about warehouse and transport functions, effeteness of clients requests using information technologies. The similar programs analysis. Not formally and formally Z language warehouse system descripting. General super market and warehouse PLA model preparation with aggregate scheme and with conceptual model and with formal specification. Also transitions and output operations. Then this general model use for super markets and warehouses and make aggregate scheme. Then integrate efficiency of logistic centres evaluated function. Formal Z and PLA metods coupling to create warehouse imitation model. In conclusion presented analysis work results.