Tampere University of Technology

TUTCRIS Research Portal

Applying finite state process algebra to formally specify a computational model of security requirements in the key2phone-mobile access solution

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review


Original languageEnglish
Title of host publicationLecture Notes in Computer Science
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783319194578
Publication statusPublished - 2015
Publication typeA4 Article in a conference publication
EventFormal Methods for Industrial Critical Systems - , United Kingdom
Duration: 1 Jan 2000 → …

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


ConferenceFormal Methods for Industrial Critical Systems
CountryUnited Kingdom
Period1/01/00 → …


Key2phone is a mobile access solution which turns mobile phone into a key for electronic locks, doors and gates. In this paper, we elicit and analyse the essential and necessary safety and security requirements that need to be considered for the Key2phone interaction system. The paper elaborates on suggestions/solutions for the realisation of safety and security concerns considering the Internet of Things (IoT) infrastructure. The authors structure these requirements and illustrate particular computational solutions by deploying the Labelled Transition System Analyser (LTSA), a modelling tool that supports a process algebra notation called Finite State Process (FSP). While determining an integrated solution for this research study, the authors point to key quality factors for successful system functionality.

Publication forum classification

Field of science, Statistics Finland