within
Hanne Riis Nielson
Chapter
Whenever data is communicated outside a security domain there is the risk that it may influence data coming back in a way that is not permitted by the security domain. This may arise when different security do...
Chapter
We develop a lightweight approach to information flow control that interacts with the use of cryptographic schemes. The language is a version of Dijkstra’s Guarded Commands language extended with parallelism, ...
Chapter and Conference Paper
We develop an approach to security of adaptive agents that is based on respecting the local security policies of agents rather than imposing a global security policy on all agents. In short, an agent can be as...
Book and Conference Proceedings
21st IFIP WG 6.1 International Conference, COORDINATION 2019, Held as Part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Kongens Lyngby, Denmark, June 17–21, 2019, Proceedings
Chapter
Programs are written in programming languages and in this chapter we are going to show how we can construct program graphs for all programs in a programming language. The programming language will be the (prob...
Chapter
Program analysis is an approach to finding properties of programs and it can be fully automated unlike program verification. The price to pay is that we can only express approximate behaviours of programs and ...
Chapter
Model checking is an approach to finding properties of programs. It can be fully automated but its efficiency is usually not as good as that of program analysis. The gain is that the precision is closer to tha...
Chapter
So far we have been looking at individual programs running on their own. In this chapter we will illustrate how to deal with concurrently running programs that may communicate with one another. Our main focus ...
Chapter
Sometimes we need to be very precise about the behaviour of our programs – there may be constructs in our programming language that are subtle or novel. Semantics is the part of Computer Science that deals wit...
Chapter
It is essential that programs are correct – meaning that their behaviour is as we intend. For example, a sorting routine should indeed sort the array given as input. To verify the correctness of programs one ofte...
Chapter
Security is becoming increasingly important and formal methods offer powerful techniques for ensuring it. There are three important components in security: Confidentiality, meaning that private data is not made p...
Chapter
Procedures (or functions) are found in most programming languages and provide a means for reusing code in a number of programming tasks. In this chapter we will illustrate how to add procedures to the Guarded ...
Chapter
We extend Alternation-Free Least Fixed Point Logic to be based on Belnap logic, while maintaining the close correspondence between static analysis and model checking pioneered by Bernhard Steffen, and opening ...
Chapter
We develop a type system for identifying the information flow between variables in a program in the Guarded Commands language. First we characterise the types of information flow that may arise between variables ...
Chapter and Conference Paper
We develop a modular approach to statically analyse imperative processes communicating by synchronous message passing. The approach is modular in that it only needs to analyze one process at a time, but will i...
Chapter and Conference Paper
One of the key demands of cyberphysical systems is that they meet their safety goals. Timed automata has established itself as a formalism for modeling and analyzing the real-time safety aspects of cyberphysical ...
Chapter
One of the key demands of cyberphysical systems is that they meet their safety goals. Timed Automata has established itself as a formalism for modelling and analysing the real-time safety aspects of cyberphysical...
Chapter and Conference Paper
Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we st...
Chapter and Conference Paper
The security validation of practical computer systems calls for the ability to specify and verify information flow policies that are dependent on data content. Such policies play an important role in concurren...
Chapter and Conference Paper
For supporting the design of self-adaptive computing systems, the PSCEL language offers a principled approach that relies on declarative definitions of adaptation and authorisation policies enforced at runtime...
