Throughout the history of computer science, a major challenge has been how to assert that software is free of bugs and works as intended. Software bugs can lead to serious negative impacts on any... Show moreThroughout the history of computer science, a major challenge has been how to assert that software is free of bugs and works as intended. Software bugs can lead to serious negative impacts on any software system. Throughout the main body of the thesis, we implemented a series of studies on exploring ways to apply formal methods systematically for the verification of complex object-oriented libraries such as the Java Collection Framework. We start with specifying and verifying methods in the java.util.LinkedList class, but we encounter challenges with methods that take an interface type as a parameter. To address this, we proposed to use histories as method calls and returns to completely determine the concrete state of any implementation and thus can be seen as a way to reason about the interface. The executable history-based (EHB) approach embeds histories and attributes directly as Java objects. This approach could be seamlessly integrated in the KeY theorem prover itself. However, the EHB approach still has its limitations, particularly when it comes to reasoning about the heap and properties of user-defined attributes.To mitigate this, we introduce the logical history-based (LHB) approach, which models histories as an external abstract data type with functions. Building on the LHB approach, we have developed a history-based refinement theory for reasoning about hierarchy in object-oriented programs. Show less
We present a framework for automata theoretic model checking of coordination systems specified in Reo coordination language. To this goal, we introduce Buchi automata of records (BAR) and their... Show moreWe present a framework for automata theoretic model checking of coordination systems specified in Reo coordination language. To this goal, we introduce Buchi automata of records (BAR) and their augmented version (ABAR) as an operational modeling formalism that covers several intended forms of behavior of Reo connectors, such as fairness, I/O synchronization, and context dependency. To specify the properties to be verified, we introduce an action based linear temporal logic, interpreted over the executions of augmented Buchi automata of records, and show how the formulas can be translated into ABARs. This translation can be done either inductively, or by using an on-the-fly method. To deal with the large state spaces, we show that ABARs can be implemented using ordered binary decision diagrams (OBDD). For this purpose, we also introduce the necessary modifications over the basic model checking algorithm that can be applied directly over OBDD structures. Our implementation and a number of case studies that we carried out show the applicability of our method over large state spaces. We also show that the state explosion problem can be tackled by compositional minimization methods using some suitable equivalence relations. In fact, we show two equivalences that are congruencies with respect to the connector composition operators and such that they both preserves linear time temporal logic properties. Show less
Complex applications such as incident management, social simulations, manufacturing applications, electronic auctions, e-institutions, and business to business applications are pervasive and... Show moreComplex applications such as incident management, social simulations, manufacturing applications, electronic auctions, e-institutions, and business to business applications are pervasive and important nowadays. Agent-oriented methodology is an advance in abstractionwhich can be used by software developers to naturally model and develop systems for suchapplications. In general, with respect to design methodologies, what it may be important tostress is that control structures should be added at later stages of design, in a natural top-downmanner going from specifications to implementations, by refinement. Too much detail (be itfor the sake of efficiency) in specifications often turns out to be harmful. To paraphrase D.E.Knuth, “Premature optimization is the root of all evil” (quoted in ‘The Unix ProgrammingEnvironment’ by Kernighan and Pine, p. 91).The aim of this thesis is to adapt formal techniques to the agent-oriented methodologyinto an executable theory of refinement. The justification for doing so is to provide correctagent-based software by design. The underlying logical framework of the theory we proposeis based on rewriting logic, thus the theory is executable in the same sense as rewriting logicis. The storyline is as follows. We first motivate and explain constituting elements of agentlanguages chosen to represent both abstract and concrete levels of design. We then proposea definition of refinement between agents written in such languages. This notion of refinement ensures that concrete agents are correct with respect to the abstract ones. The advantageof the definition is that it easily leads to formulating a proof technique for refinement viathe classical notion of simulation. This makes it possible to effectively verify refinement bymodel-checking. Additionally, we propose a weakest precondition calculus as a deductivemethod based on assertions which allow to prove correctness of infinite state agents. Wegeneralise the refinement relation from single agents to multi-agent systems in order to ensure that concrete multi-agent systems refine their abstractions. We see multi-agent systemsas collections of coordinated agents, and we consider coordination artefacts as being basedeither on actions or on normative rules. We integrate these two orthogonal coordinationmechanisms within the same refinement theory extended to a timed framework. Finally, wediscuss implementation aspects. Show less
