The research presented in this thesis concerns one of the most important questions in software engineering of our time: how can we make sure that software is free from memory safety bugs? Memory... Show moreThe research presented in this thesis concerns one of the most important questions in software engineering of our time: how can we make sure that software is free from memory safety bugs? Memory safety bugs are the major cause of common vulnerabilities and exposures, and their presence threatens the stability and security of our digital world. This question is so important that it has escalated to the highest level. In a recent White House press release (February 26, 2024), the National Cyber Director of the United States of America calls on the academic community to help solve this hard problem: “addressing [this challenge] is imperative to ensuring we can secure our digital ecosystem long-term and protect the security of our Nation.” The accompanying technical report advises on the use of memory safe programming languages, and prominently mentions formal methods as one way to achieve the highly desired freedom from bugs, including memory safety bugs.In this thesis, formal methods are studied that are used to analyze software for its correctness, where correctness means that software satisfies its specification and incorrectness means the presence of a bug. The focus is on separation logic, a formal method designed as a scalable technique in ensuring freedom from memory safety bugs. Nowadays, separation logic is a well-established field of research: it has been widely studied academically in the past twenty years, and is successfully applied on an industry-wide scale to ensure memory safety. For example, separation logic is the technique used to prove, with mathematical certainty, that memory safe programming languages (such as Rust and Go) indeed live up to the promise that “they offer a way to eliminate, not just mitigate, entire bug classes.”In two parts, this thesis presents important scientific contributions that fill a gap in the academic literature. The first part contains the missing completeness theorem for separation logic, that is on par with the fundamental result by Goedel for first-order logic. Completeness is important for any formal method as it shows that the formal method can be adequately used for demonstrating every validity. The second part finally introduces dynamic separation logic that gives an alternative way to analyze memory safety problems, such that now it is possible to prove elementary specifications without needing extra logical techniques. This is important because it ensures ‘backwards compatibility’ with automated reasoning techniques that are optimized for first-order logic. Show less
We strive to address the challenge of constructing a modeling language to write software which can take advantage of recent hardware developments (multicore, cloud) without compromising in its... Show moreWe strive to address the challenge of constructing a modeling language to write software which can take advantage of recent hardware developments (multicore, cloud) without compromising in its abstraction levels. Our language is based on top of the Abstract Behavioral Specification (ABS), which is an executable modeling language with a focus on cooperative-multitasking concurrency. We translate programs written in ABS to Haskell, an established functional programming language, since Haskell supports both cooperative concurrency in the form of coroutines, and multicore parallelism through lightweight threads of execution. Further, we formally prove the correctness as well as the resource-consumption preservation of the translation of a subset of our language to Haskell.To enable software models take control of their computing resources, we extend our language with certain constructs that abstract over the hardware. This resource-aware language extension is packaged in a tool-suite for human-in-the-loop simulation of Cloud services; such a live simulation can be used for training DevOps to the cloud environment of IT companies.Finally, we provide an implementation of distributed communication to the Cloud infrastructure, so that software models written in ABS can be executed as distributed applications, which can programmatically monitor and control their own Cloud deployment. Show less
Many scientists are focussed on building models. We nearly process all information we perceive to a model. There are many techniques that enable computers to build models as well. The field... Show more Many scientists are focussed on building models. We nearly process all information we perceive to a model. There are many techniques that enable computers to build models as well. The field of research that develops such techniques is called Machine Learning. Many research is devoted to develop computer programs capable of building models (algorithms). Many of such algorithms exist, and these often consist of various options that subtly influence performance (parameters). Furthermore, there is mathematical proof that there exists no single algorithm that works well on every dataset. This complicates the task of selecting the right algorithm for a given task. The field of meta-learning aims to resolve these problems. The purpose is to determine what kind of algorithms work well on which datasets. In order to do so, we developed OpenML. This is an online database on which researches can share experimental results amongst each other, potentially scaling up the size of meta-learning studies. Having earlier experimental results freely accessible and reusable for others, it is no longer required to conduct time expensive experiments. Rather, researchers can answer such experimental questions by a simple database look-up. This thesis addresses how OpenML can be used to answer fundamental meta-learning questions. Show less
Parallel programming has become essential for writing scalable programs on general hardware. Conceptually, every parallel program consists of workers, which implement primary units of sequential... Show moreParallel programming has become essential for writing scalable programs on general hardware. Conceptually, every parallel program consists of workers, which implement primary units of sequential computation, and protocols, which implement the rules of interaction that workers must abide by. As programmers have been writing sequential code for decades, programming workers poses no new fundamental challenges. What is new---and notoriously difficult---is programming of protocols. In this thesis, I study an approach to protocol programming where programmers implement their workers in an existing general-purpose language (GPL), while they implement their protocols in a complementary domain-specific language (DSL). DSLs for protocols enable programmers to express interaction among workers at a higher level of abstraction than the level of abstraction supported by today's GPLs, thereby addressing a number of protocol programming issues with today's GPLs. In particular, in this thesis, I develop a DSL for protocols based on a theory of formal automata and their languages. The specific automata that I consider, called constraint automata, have transition labels with a richer structure than alphabet symbols in classical automata theory. Exactly these richer transition labels make constraint automata suitable for modeling protocols. Show less
We describe a formal notation for DNA molecules that may contain nicks and gaps. The resulting DNA expressions denote formal DNA molecules. Different DNA expressions may denote the same molecule.... Show moreWe describe a formal notation for DNA molecules that may contain nicks and gaps. The resulting DNA expressions denote formal DNA molecules. Different DNA expressions may denote the same molecule. Such DNA expressions are called equivalent. We examine which DNA expressions are minimal, which means that they have the shortest length among all equivalent DNA expressions. Among others, we describe how to construct a minimal DNA expression for a given molecule. We also present an efficient, recursive algorithm to rewrite a given DNA expression into an equivalent, minimal DNA expression. For many formal DNA molecules, there exists more than one minimal DNA expression. We define a minimal normal form, i.e., a set of properties such that for each formal DNA molecule, there is exactly one (minimal) DNA expression with these properties. We finally describe an efficient, two-step algorithm to rewrite an arbitrary DNA expression into this normal form. Show less
Coinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. The broad applicability and rapidly increasing interest in... Show moreCoinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. The broad applicability and rapidly increasing interest in coinductive techniques is based on the theory of coalgebras, which allows one to understand and prove properties of state-based models of computation at a high level of abstraction. In this thesis we develop methods that simplify and enhance coinductive reasoning, with coalgebra as the framework of choice to obtain generally applicable techniques. In the first part, we introduce a coalgebraic framework of enhanced coinductive proof methods, which is applicable to a wide range of coinductive predicates and a wide range of state-based systems. In the second part, we propose enhancements to coinductive definition techniques based on the theory of mathematical operational semantics. Show less
To prevent a large software system from collapsing under its own complexity, its code needs to be well-structured. Ideally we want all code related to a certain feature to be grouped together _... Show moreTo prevent a large software system from collapsing under its own complexity, its code needs to be well-structured. Ideally we want all code related to a certain feature to be grouped together __called feature modularization__ and code belonging to different features not to mix __ called separation of concerns. But many concerns are known as 'cross-cutting concerns'. By their very nature their implementation needs to be spread around the code base. The software engineering discipline that has the most to gain from those properties is Software Product Line Engineering. It is concerned with the development and maintenance of multiple software systems at the same time, each possessing a different (but often overlapping) set of features. This gives rise to an additional need: The code for a given feature must not only be separated and modular; it also needs to be composable and able to deal gracefully with the presence or absence of other features. This thesis presents Abstract Delta Modeling, a formal framework developed to achieve these goals in software. The thesis is a product of the European HATS project. It formalizes the techniques of delta modeling, the main approach to variability used by HATS Show less
This doctoral dissertation describes a series of empirical investigations into representation, dissemination and coordination of software architecture design in the context of global software... Show moreThis doctoral dissertation describes a series of empirical investigations into representation, dissemination and coordination of software architecture design in the context of global software development. A particular focus is placed on model-centric and model-driven software development. Show less
Spiking neural P systems are a class of distributed and parallel computing models inspired by the neurophysiological behavior of neurons sending electrical impulses (spikes) along axons to other... Show moreSpiking neural P systems are a class of distributed and parallel computing models inspired by the neurophysiological behavior of neurons sending electrical impulses (spikes) along axons to other neurons. In this thesis, we consider that the spiking neural P systems are universal even if the systems work in limited asynchronous mode. And we also investigated different variants of spiking neural P systems with other additional features, such as the axon functioning, the growth of dendritic trees in neurons, the positive or negative weights on synapses, and the astrocytes having excitatory and inhibitory influence on synapses. Show less
Present-day embedded software systems need to support an increasing number of features and formalisms; the two most important ones being handling of real-time, and the possibility to develop the... Show morePresent-day embedded software systems need to support an increasing number of features and formalisms; the two most important ones being handling of real-time, and the possibility to develop the system in a modular, component-based way. To ensure that the behaviour of the final system is correct and safe, it needs to be verified before it is being put into operation. This requires formal models to model the system, and formal methods to analyse the formal model and verify certain properties of it. In this thesis, we propose both formal models and formal methods for component-based real-time systems and their coordination patterns. We present a translation from a number of formal models into a representation in propositional logic with linear arithmetic, which allows to use well-established SAT and SMT solver tools to analyse the underlying system. We present an abstraction technique on the representation, that increases the manageable system size by removing parts that are considered irrelevant to the verification of a particular property. We prove the applicability and usability of our framework with a tool implementation, that supports the design and analysis process of component-based real-time systems. 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
The intensifying need for scalable software has motivated modular development and using systems distributed over networks to implement large-scale applications. In Service-oriented Computing,... Show moreThe intensifying need for scalable software has motivated modular development and using systems distributed over networks to implement large-scale applications. In Service-oriented Computing, distributed services are composed to provide large-scale services with a specific functionality. In this way, reusability of existing services can be increased. However, due to the heterogeneity of distributed software systems, software composition is not easy and requires additional mechanisms to impose some form of a coordination on a distributed software system. Besides functional correctness, a composed service must satisfy various quantitative requirements for its clients, which are generically called its quality of service (QoS). Particularly, it is tricky to obtain the overall QoS of a composed service even if the QoS information of its constituent distributed services is given. In this thesis, we propose Stochastic Reo to specify software composition with QoS aspects and its compositional semantic models. They are also used as intermediate models to generate their corresponding stochastic models for practical analysis. Based on this, we have implemented the tool Reo2MC. Using Reo2MC, we have modeled and analyzed an industrial software, the ASK system. Its analysis results provided the best cost-effective resource utilization and some suggestions to improve the performance of the system. 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
In this thesis, a configurable generalisation of some well-known distance measures is introduced. Parameters are given to use this metric in the area of law enforcement, but also molecular biology.... Show moreIn this thesis, a configurable generalisation of some well-known distance measures is introduced. Parameters are given to use this metric in the area of law enforcement, but also molecular biology. With a valid distance measure, it is possible to analyse data by using a dimension reduction technique. One of these techniques is analysed and extended. Show less
This thesis is concerned with two research areas in natural computing: the computational nature of gene assembly and membrane computing. Gene assembly is a process occurring in unicellular... Show moreThis thesis is concerned with two research areas in natural computing: the computational nature of gene assembly and membrane computing. Gene assembly is a process occurring in unicellular organisms called ciliates. During this process genes are transformed through cut-and-paste operations. We study this process from a theoretical point of view. More specifically, we relate the theory of gene assembly to sorting by reversal, which is another well-known theory of DNA transformation. In this way we obtain a novel graph-theoretical representation that provides new insights into the nature of gene assembly. Membrane computing is a computational model inspired by the functioning of membranes in cells. Membrane systems compute in a parallel fashion by moving objects, through membranes, between compartments. We study the computational power of various classes of membrane systems, and also relate them to other well-known models of computation. Show less
In the last years, there has been a growing interest for distributed systems both in computer science and in society. The most popular and biggest distributed system in the world is the Internet. A... Show moreIn the last years, there has been a growing interest for distributed systems both in computer science and in society. The most popular and biggest distributed system in the world is the Internet. A distributed system is a collection of independent computers that appears to its users as a single coherent system. These computers are connected to each other through a network. On each of these computers there is at least one (software) component that needs to communicate with other components on remote computers to achieve some goal. Components can consist of processes, databases, applications, etc. These components are not only distributed among the several computers of a network but they also run in parallel. Therefore, distributed systems need appropriate theory and infrastructures for the coordination of its concurrently running components. In this thesis we present MoCha, a novel coordination framework. MoCha allows dynamic reconfiguration of connections among the components in a system, a property that is very useful and even crucial in systems where the components themselves are mobile. Furthermore, MoCha provides exogenous coordination. This makes it possible to coordinate components from the 'outside' (exogenous), and thus, change a distributed system's behavior without having to change its components. Show less
Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes... Show moreBesides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes shared-variable concurrency via instance variables, coordination via reentrant synchronization monitors, synchronous message passing, and dynamic thread creation. To reason about safety properties of multithreaded Java programs, we introduce a tool-supported assertional proof method for JavaMT ("Multi-Threaded Java"), a small sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java. The verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behavior of a single instance, and global ones taking care of the connections between objects. We establish the soundness and the completeness of the proof system. From an annotated program, a number of verification conditions are generated and handed over to the interactive theorem prover PVS. Show less
