This thesis introduces correctness-by-construction techniques for rigorous system design. In particular, we focused on how to produce and validate a functional application model from a set of requirements or from application code. First, we dealt with the early validation of system requirements and design, in order to eliminate the need for a-posteriori verification at the later stages of development. Second, we focused on the automated generation of functional application models from programs with nested syntax, while maintaining the program semantics. Finally, we proposed a design flow that aims to maintain the consistency between the application model and the application code, using a new domain-specific language that focuses on the design of resource-constrained applications for the Internet of Things.

Given a transition system M and a specification formula f, the problem of model checking is to determine if M satisfies f. An extended problem of model checking is that of model repair. In the case that M violates f, the problem of model repair is to obtain a new model M΄, such that M΄ satisfies f. Moreover, the changes made to M to derive M΄ should be minimum with respect to all such M΄. As in model checking, state explosion can make it virtually impossible to carry out model repair on models with infinite or even large state spaces. This thesis examines the problem of model repair for (i) Kripke structures and Computation Tree Logic and, (ii) probabilistic systems and reachability temporal logic properties. For Kripke structures, this thesis presents a framework for model repair that uses abstraction refinement to tackle state space explosion. The proposed framework aims to repair Kripke Structure models based on a Kripke Modal Transition System abstraction and a 3-valued semantics for CTL. An abstract-model-repair algorithm is introduced for which soundness and semi-completeness are proven, and its complexity class is studied. Moreover, a prototype implementation is presented to illustrate the practical utility of abstract model repair on an Automatic Door Opener system model and a model of the Andrew File System 1 protocol. For probabilistic systems, this thesis presents a framework based on abstraction and re#nement, which reduces the state space of the probabilistic system to repair at the price of obtaining an approximate solution. A metric space is defined over the set of DTMCs, in order to measure the differences between the initial and the repaired models. For the repair, this thesis introduces an algorithm and discusses its important properties, such as soundness and complexity. As a proof of concept, experimental results are provided for probabilistic systems with diverse structures of state spaces, including thewell-known Craps game, the IPv4 Zeroconf protocol, a message authentication protocol and the gambler's ruin model.

Modern network centric information systems implement highly distributed architectures that usually include multiple application servers. Application design is mainly based on the fundamental object—oriented principles and the adopted architecture matches the logical decomposition of applications into several tiers such as presentation, logic and data to their software and hardware structuring. Transactions offer a convenient mechanism for structuring distributed workloads due to the ACID properties (Atomicity, Consistency, Isolation, Durability). For some applications however, the ACID properties are too restrictive. In mobile computing or in web applications for example, long intervals of non—responsiveness or frequent disconnections lead to long—running transactions that may block concurrently running transactions and render acquired resources unavailable to other processes. New transaction models often relax one of the ACID properties in order to cope with the challenges of the aforementioned execution environments. In transactional memory for example, consistency and durability guaranties are not provided. The new transaction models, often termed as advanced transactions, may not fulfill some intended properties. Formal specification and reasoning for transaction properties is essential for proving the validity of transaction models, but it has been limited to proof—theoretic approaches despite the recent progress in model checking. Moreover, we have not seen so far automated techniques that can derive a correct implementation from a valid transaction model. Performance and availability of transaction processing depends on the adopted architectural design for a given transaction model. Design decisions have measurable effects on availability and performance of transaction processing systems. Existing trade—offs among the design factors of an architecture affect the quality of the transaction processing service in a complex manner.
In order to address the discussed problems, we introduce a model—driven architecture based approach with a two—fold contribution.
First, we provide a systematic process for model checking a transaction model and automatically generate a correct implementation. Models are specified by state machines that represent interacting transactional entities synchronized on a set of events. Verification is performed by examining all possible execution paths of the synchronized state machines for property violations.
Second, we elaborate on an approach for discovering architecture trade—offs and for evaluating the impact of design decisions on performance and availability. The proposed method is applicable on experimental data obtained by simulation or from a prototype implementation. If an architecture design fails to fulfil the performance and availability goals for the considered workloads, the method is iteratively applied towards modifying the initial architecture until the goals are achieved.
The aforementioned contributions are part of a process for the development of transaction systems that we believe is capable to cope with the inherent complexity of distributed transaction processing.

Nowadays, the spread of computer networks and internet communications increases rapidly, causing an even strong need for quality of services, but mostly, the security of them. The present doctorate thesis involves with the verification of security protocols with the use of formal methods.
The research been conducted, studies the security guaranties that most of the modern security protocols, tend to offer to the participant entities. Related work has shown that in order to successfully verify a security protocol, it is a necessity to check the protocol correctness while operating with a strong intruder entity. Using automatic model checking tools, we have developed discrete formal method techniques that combined with the proposed intruder theories can be useful for the correctness and the exhaustive verification of a series of security properties. Using these intruder theories, we verify security protocols’ tolerance against common attack policies that can be applied today by dishonest protocol users.
One of the major problems found today in the research area of formal methods is the known problem of the State Space explosion. When modeling a system using model checking, the produced state space may increase dramatically due to the complexity of the processed involved in the model or for example the mechanisms that are embedded into (e.g. random generator number machine, cryptographic functions). Furthermore, the combination of a powerful intruder model into the security system may lead to an enormous state space, resulting in a difficult and time-consuming security analysis.
In the present thesis, three distinct intruder theories and models have been developed in order to guide the analysts into a much easier analysis of their security protocols. While the analyst today may find a wide area of security properties that target towards verification of them, the described intruder theories provide a selection for the appropriate intruder model - depending on the properties - to be applied, providing a successful verification mean, into revealing potential security flaws. We formally describe these three intruder theories and verify their success over a series of security protocols. As a result, the proposed intruders have not only dramatically decreased the produced state space during model checking but also they have been proved capable of revealing unknown to us security flaws in the tested protocol systems.
To conclude, the contribution of this thesis lies in the successful verification of the security guaranties of security protocols, with the help of specific intruder models, which are independent from the used mean of communication by the protocols’ participants. Using the developed powerful intruder creation methodologies, the analyst may exhaustively check its protocol for security flaws, using formal methods techniques, without producing a large state space that could lead its analysis impossible to be conducted.

Οι σύγχρονες ανάγκες επεξεργασίας δεδομένων οδηγούν στην ανάπτυξη κατανεμημένων διατάξεων αρχιτεκτονικής πελάτη - διακομιστή (client - server). Κάθε νέο υπολογιστικό σύστημα αποτελείται πλέον από ένα σύνολο τμημάτων υλικού και λογισμικού, πιθανώς διαφορετικών τεχνολογιών ή και διαφορετικών κατασκευαστών, η διασύνδεση των οποίων υποστηρίζεται από σταθμούς εργασίας - μέλη ενός δικτύου.
Μέσα σ' αυτό το πλαίσιο, ο εντοπισμός των παραγόντων που επιδρούν καθοριστικά στην απόδοση και η εκτίμηση αυτής σε εναλλακτικές περιπτώσεις διαμόρφωσης του συστήματος προϋποθέτουν την υιοθέτηση μιας νέας προσέγγισης, πέρα από την κλασσική της χρήσης αναλυτικών ή προσομοιωτικών "επίπεδων" δικτύων ουρών.
Σκοπός της διατριβής αυτής ήταν η ανάπτυξη ή/και βελτίωση των τεχνικών εκείνων, που είναι απαραίτητες στην ανάλυση της απόδοσης λογισμικού κατανεμημένης αρχιτεκτονικής.