UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Conditional transition systems with upgrades

Beohar, H; König, B; Küpper, S; Silva, A; (2018) Conditional transition systems with upgrades. In: Proceedings of the International Symposium on Theoretical Aspects of Software Engineering (TASE) 2017. (pp. pp. 1-8). IEEE: Danvers (MA), USA. Green open access

[thumbnail of Silva_Conditional transition systems with upgrades_AAM.pdf]
Preview
Text
Silva_Conditional transition systems with upgrades_AAM.pdf

Download (309kB) | Preview

Abstract

We introduce a variant of transition systems, where activation of transitions depends on conditions of the environment and upgrades during runtime potentially create additional transitions. Using a cornerstone result in lattice theory, we show that such transition systems can be modelled in two ways: as conditional transition systems (CTS) with a partial order on conditions, or as lattice transition systems (LaTS), where transitions are labelled with the elements from a distributive lattice. We define equivalent notions of bisimilarity for both variants and characterise them via a bisimulation game. We explain how conditional transition systems are related to featured transition systems for the modelling of software product lines. Furthermore, we show how to compute bisimilarity symbolically via BDDs by defining an operation on BDDs that approximates an element of a Boolean algebra into a lattice. We have implemented our procedure and provide runtime results.

Type: Proceedings paper
Title: Conditional transition systems with upgrades
Event: International Symposium on Theoretical Aspects of Software Engineering (TASE)
Location: Sophia Antipolis, France
Dates: 13th-15th September 2017
ISBN-13: 978-1-5386-1924-7
Open access status: An open access version is available from UCL Discovery
DOI: 10.1109/TASE.2017.8285624
Publisher version: https://doi.org/10.1109/TASE.2017.8285624
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: Lattices, Boolean algebra, Runtime, Software product lines, Encryption, Games
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10060796
Downloads since deposit
44Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item