arXiv subjects

Sabine Glesner

Publications and source records attributed to Sabine Glesner.

3 recordsLinked to original sources

arXiv2015

A Denotational Semantics for Communicating Unstructured Code

An important property of programming language semantics is that they should be compositional. However, unstructured low-level code contains goto-like commands making it hard to define a semantics that is compositional. In this paper, we follow the ideas of Saabas and Uustalu to structure low-level code. This gives us the possibility to define a compositional denotational semantics based on least fixed points to allow for the use of inductive verification methods. We capture the semantics of communication using finite traces similar to the denotations of CSP. In addition, we examine properties of this semantics and give an example that demonstrates reasoning about communication and jumps. With this semantics, we lay the foundations for a proof calculus that captures both, the semantics of unstructured low-level code and communication.

cs.PL↗

arXiv2013

Towards a Formal Framework for Mobile, Service-Oriented Sensor-Actuator Networks

Service-oriented sensor-actuator networks (SOSANETs) are deployed in health-critical applications like patient monitoring and have to fulfill strong safety requirements. However, a framework for the rigorous formal modeling and analysis of SOSANETs does not exist. In particular, there is currently no support for the verification of correct network behavior after node failure or loss/addition of communication links. To overcome this problem, we propose a formal framework for SOSANETs. The main idea is to base our framework on the π-calculus, a formally defined, compositional and well-established formalism. We choose KLAIM, an existing formal language based on the π-calculus as the foundation for our framework. With that, we are able to formally model SOSANETs with possible topology changes and network failures. This provides the basis for our future work on prediction, analysis and verification of the network behavior of these systems. Furthermore, we illustrate the real-life applicability of this approach by modeling and extending a use case scenario from the medical domain.

cs.NI↗

arXiv1999

Combining Inclusion Polymorphism and Parametric Polymorphism

We show that the question whether a term is typable is decidable for type systems combining inclusion polymorphism with parametric polymorphism provided the type constructors are at most unary. To prove this result we first reduce the typability problem to the problem of solving a system of type inequations. The result is then obtained by showing that the solvability of the resulting system of type inequations is decidable.

cs.LO↗