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

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

    3 Citations (Scopus)
    59 Downloads (Pure)

    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
    Pages94-113
    Number of pages20
    ISBN (Electronic)978-3-319-47166-2
    ISBN (Print)978-3-319-47165-5
    DOIs
    Publication statusPublished - Oct 2016
    Event7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2016 - Corfu, Greece
    Duration: 10 Oct 201614 Oct 2016
    Conference number: 7
    http://www.isola-conference.org/isola2016/

    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

    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. https://doi.org/10.1007/978-3-319-47166-2_7