Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 18:00 - 18:20 at Sala VII - Session 4 Chair(s): Adrian Francalanza, Jorge A. Pérez

A typical IoT sensor device is built from several independent components that cooperate together to sense and actuate on the physical world. Programming these devices can easily cause hardware failures that are not usually considered in general programming languages. For instance, programs can easily run out of memory causing the device simply to reboot; a mistake in a loop can render the device unusable, as it can drain its battery. As the program runs on the bare metal (there is no operating system nor device drivers), the program can improperly use the hardware, which, in most of the cases, leads to the action to be silently ignored. For example, by loosing a message that was sent when the device was not ready to send, or by manipulating a non-existent or misconfigured LED (Light-Emitting Diode).

We use behavioural types to describe the hardware as a set of well-defined components with valid interdependencies, in the spirit of the multiparty session types [1]. Our type describes each component per se in terms of its interface and its behaviour. The former defines the actions that the device makes available and the events the device triggers; the latter specifies the order in which actions and events can occur. As usual, in behavioural type works, our goal is to verify that the components are assembled correctly as a valid component (well typed), and that the programs use the device according to the prescribed type. Additionally, we want to express temporal-logic propositions on traces, so that we can prove, for instance, that a modem is always disconnected before the device enters the sleep state. To the best of our knowledge no IoT framework incorporates such analysis.

In this talk we present a simple hardware device and use our types to describe several increasingly complex behaviours of this device, thus assessing the informal expressiveness of our types. We discuss on how to verify that the behaviour of a component is a valid composition of simpler components. Finally, we hint on how to check that programs comply with a component type.

Hardware Interactions As Behavioural Types (beat2019-presentation.pdf)5.64MiB

Sun 13 Jan

beat-2019-papers
16:00 - 18:25: BEAT 2019 - Session 4 at Sala VII
Chair(s): Adrian FrancalanzaUniversity of Malta, Jorge A. PérezUniversity of Groningen, The Netherlands
beat-2019-papers16:00 - 16:50
Talk
beat-2019-papers16:50 - 17:10
Talk
Evangelia VaneziUniversity of Cyprus, Dimitrios KouzapasUniversity of Cyprus, Anna PhilippouUniversity of Cyprus
beat-2019-papers17:10 - 17:30
Talk
Daniele Nantes-SobrinhoUniversity of Brasília, Brazil, Jorge A. PérezUniversity of Groningen, The Netherlands
beat-2019-papers17:30 - 17:40
Break
beat-2019-papers17:40 - 18:00
Talk
Søren DeboisIT University of Copenhagen, Thomas H. Hildebrandt, Hugo LópezIT University of Copenhagen, Denmark & DCR Solutions A/S
Media Attached
beat-2019-papers18:00 - 18:20
Talk
Carlos Mão de FerroLASIGE, Faculty of Sciences, University of Lisbon, Francisco MartinsLaSIGE, University of Lisbon, Tiago CogumbreiroUniversity of Massachusetts Boston
File Attached
beat-2019-papers18:20 - 18:25
Day closing
Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS, Jorge A. PérezUniversity of Groningen, The Netherlands