Abstract: Software is expected to behave in a deterministic fashion. However, determinism is hard to attain in concurrent programs because the interleaved execution of concurrent threads in a program may change each time a program is run, which changes also the thread interferes through their reordered access of shared resources. Furthermore, previous reasoning techniques like operational reasoning were deemed impractical for concurrent programs due to having an exhaustive case analysis of the thread interleaving [1]. This complicates correct programs' construction and modular reasoning about such programs. We plan to extend existing work [1] applying separation based reasoning to message passing concurrency. In particular, this present work can only handle value passing concurrency, whereby the channel connections between the interacting processes is fixed. We plan to extend this so as to be able to handle channel passing, where channels are communicated on other channels, which makes the channel topology dynamic. The present work is also limited in a few other ways: it can handle only limited forms of computation flows as well as limited forms of permission transfers for analyzing determinism. We shall be looking at ways how to address these limitations thereby extending the pool of programs that the logic can handle.

References:
[1] Permission-Based Seperation Logic for Message-Passing Concurrency, Adrian Francalanza, Julian Rathke, Vladimiro Sassone, LMCS (to appear), 2010.

Abstract: The complexity of computer systems has been growing for a number of years, and therefore it has become very difficult for developers to verify correctness of such systems. As their complexity continues to grow, the number of bugs found is increasing. Traditionally, software errors are analyzed using either model checking which suffers from state-explosion problem or testing, which suffers from coverage problems. Recently, researchers started using runtime monitors to verify correctness. However, developing monitors that adheres to some correctness specification is not trivial and can itself introduce bugs within the code of the monitor.
This project investigates how monitors that exhibit soundness and completeness can be automatically generated from the logic of a property language. Focus will be given on automatically synthesizing sound monitors in a concurrent language from a modal temporal logic. In particular, we will consider the Hennessy-Milner Logic (HML) as our base logic for specifying properties and translate to a process calculus such as Milner's Calculus of Communicating Systems (CCS) and the pi-calculus. The aim of this project is to formalize a proof that is able to automatically synthesize sound and potentially complete monitors from property language. This proof will act as a direct model that can be used to implement a runtime monitor or as a guiding principle for the construction of new real time monitor.

Abstract: When developing and marketing software that controls safety critical systems, embedded systems or reactive systems such as software controlling an artificial pacemaker and communication systems, it is highly important to have a verification process that makes sure that the software is always behaving properly. This enables the possibilities of giving realistic guarantees on what the software will actually do and what it will never do. One possible solution to give these guarantees is to provide a monitor program that continuously checks the behaviour of the system and raises a warning or takes an action when the behaviour is not correct. This concept is commonly referred to Runtime Verification or Runtime Monitoring.
With the current knowledge that we have, the monitoring code that checks whether the system behaviour is correct or not has to be developed manually according to some specification. However, this raises the possibility that errors can be introduced in the monitor and might give false-alarms or even worse signal 'ok' when the system is not actually correct. In this project, the aim is to develop a formally verified tool for Erlang programs that given a correctness specification property, automatically generates a monitor that tests for this property. The tool will also be able to terminate an ill-behaving system and replace the execution with a formally verified program using techniques such as model checking with tools such as McErlang. The tool shall target Erlang programs and can thus be used for existing systems and ease the introduction of Runtime Monitoring in such systems without the need for strong theoretical background.

Abstract: Distributed algorithms are nowadays found in wide range of applications. Such algorithms consist of concurrent, co-operating processes which interact towards the same goal. Despite the importance of distributed algorithms to be well-behaved, correctness proofs of such algorithms are often informal. Conventionally algorithms and their specifications (correctness criteria) are described using semi-formal pseudo code, and thus their correctness proofs then follow this same semi-formal style. This current status quo of distributed algorithms gives rise to two main problems. First is the discrepancy between the semi-formal described algorithms and the actual implementation of the algorithms using formal languages, which may induce errors in the deployment of these algorithms. Second, the concurrent nature of distributed algorithms makes them notoriously difficult due to the exponential number of interleavings amongst the parallel processes and subtle interfaces at these interleavings. Semiformal descriptions and proofs then gloss over these subtleties. Process calculi are conventionally used to formally model concurrent systems and come equipped with a rich formal theory (such as bisimulation equivalence). For such reasons process calculi are a natural choice to counter act the afore mentioned problems, but this approach is still no panacea, as correctness proofs become complex and relatively large in size, consequently obscuring the key steps of the proof.
This project will be addressing afore mentioned shortcomings of the current status quo by extending the study presented by Francalanza et al. [1]. This prior work has proposed a prescriptive methodology for studying distributed algorithms. Despite being based on bisimulation, this methodology still manages to tame the complexity brought about by this formalism. The mitigation of such complexity is attained through the idea of decomposing monolithic proofs into multi-staged proofs. Concrete stages of these multi-staged proofs include; correctness proofs of the distributed algorithm in a failure free environment, and the correctness preservation proofs of the same algorithm under failures. Through the formalization and correctness proofs of a selection of distributed algorithms, this project will attempt to give a better comprehensive assessment of the applicability of the methodology proposed by Francalanza and Hennessy [1].

References:
[1] A Fault Tolerance Bisimulation Proof For Consensus. Adrian Francalanza and Matthew Hennessy, ESOP (European Symposium on Programming) 2007: 395-410.