Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO

  • 1 Citations

Abstract

Streaming applications for mobile platforms impose high demands on a system’s throughput and energy consumption. Dynamic system-level techniques have been introduced, to reduce power consumption at the expense of performance. We consider DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling). The complex programming task now includes mapping and scheduling every task onto a heterogeneous multi-processor hardware platform. Moreover, DPM and DVFS parameters must be controlled, to meet all throughput constraints while minimizing the energy consumption. Previous work proposed to automate this process, by modeling streaming applications in SDF (Synchronous Data Flow), modeling the processor platform, translating both models to PTA (Priced Timed Automata, where prices model energy), and using Uppaal Cora to compute energy-optimal schedules that adhere to the throughput constraints. In this paper, we experiment with an alternative approach, based on stochastic hybrid games. We investigate the applicability of Uppaal Stratego to first synthesize a permissive controller satisfying a throughput constraint, and then select a near-optimal strategy that additionally minimizes the energy consumption. Our goal is to compare the Uppaal Cora and Uppaal Stratego approaches in terms of modeling effort, results and computation times, and to reveal potential limitations.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques
Subtitle of host publication7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I
EditorsTiziana Margaria, Bernhard Steffen
Place of PublicationLondon
PublisherSpringer Verlag
Pages94-113
Number of pages20
ISBN (Electronic)978-3-319-47166-2
ISBN (Print)978-3-319-47165-5
DOIs
StatePublished - Oct 2016
Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece

Publication series

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

Conference

Conference7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016
Abbreviated titleISoLA 2016
CountryGreece
CityCorfu
Period10/10/1614/10/16
Internet address

Fingerprint

Throughput
Energy utilization
Controllers
Dynamical systems
Electric power utilization
Scheduling
Hardware
Experiments
Voltage scaling
Dynamic frequency scaling
Power management

Keywords

  • IR-102545
  • EWI-27297
  • EC Grant Agreement nr.: FP7/318490
  • METIS-319459
  • Adaptive Systems
  • Compilers
  • Formal Methods
  • Formal verification
  • Model checking
  • model-driven engineering
  • Modeling
  • Privacy
  • Programming languages
  • Railways
  • Refinement
  • Security
  • Semantics
  • Service-Oriented Architecture (SOA)
  • Software engineering
  • Software Evolution
  • Software product lines
  • Specifications
  • Static Analysis
  • Unified modeling language

Cite this

Ahmad, W., & van de Pol, J. C. (2016). Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I (pp. 94-113). (Lecture Notes in Computer Science; Vol. 9952). London: Springer Verlag. DOI: 10.1007/978-3-319-47166-2_7

Ahmad, W.; van de Pol, Jan Cornelis / Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO.

Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. London : Springer Verlag, 2016. p. 94-113 (Lecture Notes in Computer Science; Vol. 9952).

Research output: Scientific - peer-reviewConference contribution

@inbook{64788eecf72749b69484fb2d24326ad5,
title = "Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO",
abstract = "Streaming applications for mobile platforms impose high demands on a system’s throughput and energy consumption. Dynamic system-level techniques have been introduced, to reduce power consumption at the expense of performance. We consider DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling). The complex programming task now includes mapping and scheduling every task onto a heterogeneous multi-processor hardware platform. Moreover, DPM and DVFS parameters must be controlled, to meet all throughput constraints while minimizing the energy consumption. Previous work proposed to automate this process, by modeling streaming applications in SDF (Synchronous Data Flow), modeling the processor platform, translating both models to PTA (Priced Timed Automata, where prices model energy), and using Uppaal Cora to compute energy-optimal schedules that adhere to the throughput constraints. In this paper, we experiment with an alternative approach, based on stochastic hybrid games. We investigate the applicability of Uppaal Stratego to first synthesize a permissive controller satisfying a throughput constraint, and then select a near-optimal strategy that additionally minimizes the energy consumption. Our goal is to compare the Uppaal Cora and Uppaal Stratego approaches in terms of modeling effort, results and computation times, and to reveal potential limitations.",
keywords = "IR-102545, EWI-27297, EC Grant Agreement nr.: FP7/318490, METIS-319459, Adaptive Systems, Compilers, Formal Methods, Formal verification, Model checking, model-driven engineering, Modeling, Privacy, Programming languages, Railways, Refinement, Security, Semantics, Service-Oriented Architecture (SOA), Software engineering, Software Evolution, Software product lines, Specifications, Static Analysis, Unified modeling language",
author = "W. Ahmad and {van de Pol}, {Jan Cornelis}",
year = "2016",
month = "10",
doi = "10.1007/978-3-319-47166-2_7",
isbn = "978-3-319-47165-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "94--113",
editor = "Tiziana Margaria and Bernhard Steffen",
booktitle = "Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques",

}

Ahmad, W & van de Pol, JC 2016, Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, Springer Verlag, London, pp. 94-113, 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016, Corfu, Greece, 10-14 October. DOI: 10.1007/978-3-319-47166-2_7

Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO. / Ahmad, W.; van de Pol, Jan Cornelis.

Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. ed. / Tiziana Margaria; Bernhard Steffen. London : Springer Verlag, 2016. p. 94-113 (Lecture Notes in Computer Science; Vol. 9952).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO

AU - Ahmad,W.

AU - van de Pol,Jan Cornelis

PY - 2016/10

Y1 - 2016/10

N2 - Streaming applications for mobile platforms impose high demands on a system’s throughput and energy consumption. Dynamic system-level techniques have been introduced, to reduce power consumption at the expense of performance. We consider DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling). The complex programming task now includes mapping and scheduling every task onto a heterogeneous multi-processor hardware platform. Moreover, DPM and DVFS parameters must be controlled, to meet all throughput constraints while minimizing the energy consumption. Previous work proposed to automate this process, by modeling streaming applications in SDF (Synchronous Data Flow), modeling the processor platform, translating both models to PTA (Priced Timed Automata, where prices model energy), and using Uppaal Cora to compute energy-optimal schedules that adhere to the throughput constraints. In this paper, we experiment with an alternative approach, based on stochastic hybrid games. We investigate the applicability of Uppaal Stratego to first synthesize a permissive controller satisfying a throughput constraint, and then select a near-optimal strategy that additionally minimizes the energy consumption. Our goal is to compare the Uppaal Cora and Uppaal Stratego approaches in terms of modeling effort, results and computation times, and to reveal potential limitations.

AB - Streaming applications for mobile platforms impose high demands on a system’s throughput and energy consumption. Dynamic system-level techniques have been introduced, to reduce power consumption at the expense of performance. We consider DPM (Dynamic Power Management) and DVFS (Dynamic Voltage and Frequency Scaling). The complex programming task now includes mapping and scheduling every task onto a heterogeneous multi-processor hardware platform. Moreover, DPM and DVFS parameters must be controlled, to meet all throughput constraints while minimizing the energy consumption. Previous work proposed to automate this process, by modeling streaming applications in SDF (Synchronous Data Flow), modeling the processor platform, translating both models to PTA (Priced Timed Automata, where prices model energy), and using Uppaal Cora to compute energy-optimal schedules that adhere to the throughput constraints. In this paper, we experiment with an alternative approach, based on stochastic hybrid games. We investigate the applicability of Uppaal Stratego to first synthesize a permissive controller satisfying a throughput constraint, and then select a near-optimal strategy that additionally minimizes the energy consumption. Our goal is to compare the Uppaal Cora and Uppaal Stratego approaches in terms of modeling effort, results and computation times, and to reveal potential limitations.

KW - IR-102545

KW - EWI-27297

KW - EC Grant Agreement nr.: FP7/318490

KW - METIS-319459

KW - Adaptive Systems

KW - Compilers

KW - Formal Methods

KW - Formal verification

KW - Model checking

KW - model-driven engineering

KW - Modeling

KW - Privacy

KW - Programming languages

KW - Railways

KW - Refinement

KW - Security

KW - Semantics

KW - Service-Oriented Architecture (SOA)

KW - Software engineering

KW - Software Evolution

KW - Software product lines

KW - Specifications

KW - Static Analysis

KW - Unified modeling language

U2 - 10.1007/978-3-319-47166-2_7

DO - 10.1007/978-3-319-47166-2_7

M3 - Conference contribution

SN - 978-3-319-47165-5

T3 - Lecture Notes in Computer Science

SP - 94

EP - 113

BT - Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques

PB - Springer Verlag

ER -

Ahmad W, van de Pol JC. Synthesizing Energy-Optimal Controllers for Multiprocessor Dataflow Applications with UPPAAL STRATEGO. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016, Proceedings, Part I. London: Springer Verlag. 2016. p. 94-113. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-47166-2_7