Modeling and analysis of cyber-physical systems are still challenging. One reason is that cyber-physical systems involve many different parts (cyber or physical), of different nature (discrete or... Show moreModeling and analysis of cyber-physical systems are still challenging. One reason is that cyber-physical systems involve many different parts (cyber or physical), of different nature (discrete or continuous), and in constant interaction via sensing and actuating.For instance, consider a group of robots, each running a program that takes decision based on the sequence of sensor readings. The sensors that equip a robot return the current position of the robot and the position of any adjacent obstacle. The interactionoccurring between each robot in the group cannot be derived solely from the specification of individual robots. If the field on which the robots roam changes its property, the same group of robots might sense different values, and therefore take different actions. Also, the time at which a robot acts and senses will affect the decision of each controller and will change the resulting collective behavior.This thesis proposes a compositional approach to the design and programming of interacting cyber-physical components. We present an algebra that provides a novel perspective on modeling interaction of cyber-physical components. Using our algebraic framework, one can design a complex cyber-physical system by first designing each part, and then specifying how the parts interact. We formalized the relation between our abstract semantic model and an implementation written in Maude, a programming language based on rewriting logic. We present some applications, including safety and liveness properties of a system consisting of a set of robots, each equipped with a battery, running on a shared field. Show less
With the advent of multicore processors and data centers, computer hardware has become increasingly parallel, allowing one to run multiple pieces of software at the same time on different machines.... Show moreWith the advent of multicore processors and data centers, computer hardware has become increasingly parallel, allowing one to run multiple pieces of software at the same time on different machines. Coordination of these pieces is best expressed in a coordination language as an explicit interaction protocol that clearly defines the interactions among all components in the software. An explicit interaction protocol not only improves code structure but also enables automated analysis of the protocol to improve execution efficiency of the software. In this thesis, we focus in particular on improving execution efficiency by means of scheduling, which concerns with the allocation of (computing) resources to software tasks. Almost always, scheduling is the responsibility of a general-purpose operating system that makes no assumptions on the software and thereby ignores all relevant scheduling information in that software. As a result, the operating system alone cannot ensure optimally scheduled execution of the software. In this thesis, we propose a solution that changes the software such that it will be efficiently scheduled by the general-purpose operating system. The main idea is to take advantage of the duality between scheduling and coordination. To be precise, we analyze the protocol of the software to determine an optimal scheduling strategy for this software. Then, we enforce this optimal schedule by incorporating the strategy in the original protocol. As a result, we force the ignorant operating scheduler to follow our precomputed optimal schedule. Show less
The core contributions of this thesis target the intersection of object orientation, actor model, and concurrency. We choose Java as the main target programming language and as one of the... Show more The core contributions of this thesis target the intersection of object orientation, actor model, and concurrency. We choose Java as the main target programming language and as one of the mainstream object-oriented languages. We formalize a subset of Java and its concurrency API to facilitate formal verification and reasoning about it. We create an abstract mapping from a concurrent-object modeling language, ABS, to the programming semantics of concurrent Java. We provide the formal semantics of the mapping and runtime properties of the concurrency layer including deadlines and scheduling policies. We provide an implementation of the ABS concurrency layer as a Java API library and framework utilizing the latest language additions in Java 8. Show less
In this thesis we investigate different techniques and formalisms to address complexity introduced by unbounded structures in object-oriented programs. We give a representation of a weakest... Show moreIn this thesis we investigate different techniques and formalisms to address complexity introduced by unbounded structures in object-oriented programs. We give a representation of a weakest precondition calculus for abstract object creation in dynamic logic. Based on this calculus we define symbolic execution including abstract object creation. We investigate the complex behaviour introduced by multi-threading and give a formalism based on the transformation of multi-threaded reentrant call-graphs to thread automata and the application of context free language reachability to decide deadlock freedom of such programs. We give a formalisation of the observable interface behaviour of a concurrent, object-oriented language with futures and promises. The calculus captures the core of the Creol language and allows for a comparison with the concurrency model of thread-based, object-oriented languages like Java or C#. We give a technique to detect deadlock freedom for an Actor-like subset of the Creol language. Show less
The software today is distributed over several processing units. At a large scale this may span over the globe via the internet, or at the micro scale, a software may be distributed on several... Show moreThe software today is distributed over several processing units. At a large scale this may span over the globe via the internet, or at the micro scale, a software may be distributed on several small processing units embedded in one device. Real-time distributed software and services need to be timely and respond to the requests in time. The Quality of Service of real time software depends on how it schedules its tasks to be executed. The state of the art in programming distributed software, like in Java, the scheduling is left to the underlying infrastructure and in particular the operating system, which is not anymore in the control of the applications. In this thesis, we introduce a software paradigm based on object orientation in which real-time concurrent objects are enabled to specify their own scheduling strategy. We developed high-level formal models for specifying distributed software based on this paradigm in which the quality of service requirements are specified as deadlines on performing and finishing tasks. At this level we developed techniques to verify that these requirements are satisfied. This research has opened the way to a new approach to modeling and analysis of a range of applications such as continuous planning in the context of logistics software in a dynamic environment as well as developing software for multi-core systems. Industrial companies (DEAL services) and research centers (the Uppsala Programming for Multicore Architectures Resrearch Center UPMARC) have already shown interest in the results of this thesis. Show less
Since the inception of programming, composition of algorithms has served as the driving force behind software composition. The models and techniques that have emerged out of this focus do not... Show moreSince the inception of programming, composition of algorithms has served as the driving force behind software composition. The models and techniques that have emerged out of this focus do not adequately meet our modern requirements, such as third-party composition of black-box components, or dynamic composition of the behavior of independent distributed subsystems and services. Decades of theoretical and practical work in the field of concurrency has culminated in substantial experience with various aspects of interaction and protocols. Curiously, however, interaction has not been considered as a first-class concept in a constructive model of computation. I believe the inadequacy of our contemporary composition techniques and our neglect to treat interaction as a first-class concept are intertwined. In this lecture, I describe some of my work and ideas on a compositional model for construction of complex systems out of simpler parts, using interaction as the only first-class concept. Show less
