hh.sePublications
Change search
Link to record
Permanent link

Direct link
BETA
Publications (10 of 97) Show all publications
Chamberlain, R., Taha, W. & Törngren, M. (Eds.). (2019). Cyber Physical Systems. Model-Based Design: 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Turin, Italy, October 4–5, 2018, Revised Selected Papers (1ed.). Cham: Springer
Open this publication in new window or tab >>Cyber Physical Systems. Model-Based Design: 8th International Workshop, CyPhy 2018, and 14th International Workshop, WESE 2018, Turin, Italy, October 4–5, 2018, Revised Selected Papers
2019 (English)Conference proceedings (editor) (Refereed)
Abstract [en]

This book constitutes the proceedings of the 8th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2018 and 14th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2018, held in conjunction with ESWeek 2018, in Torino, Italy, in October 2018. The 13 full papers presented together  with 1 short paper in this volume were carefully reviewed and selected from 18 submissions. The conference presents a wide range of domains including Modeling, simulation, verification, design, cyber-physical systems, embedded systems, real-time systems, safety, and reliability. © 2019 Springer Nature Switzerland AG. Part of Springer Nature.

Place, publisher, year, edition, pages
Cham: Springer, 2019. p. 231 Edition: 1
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11615
Keywords
Modeling, Simulation, Cyber-Physical Systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-41303 (URN)10.1007/978-3-030-23703-5 (DOI)978-3-030-23703-5 (ISBN)978-3-030-23702-8 (ISBN)
Funder
Knowledge Foundation
Available from: 2019-12-24 Created: 2019-12-24 Last updated: 2020-01-15Bibliographically approved
Marchand, J., Puissochet, G., Lithén, T. & Taha, W. (2019). MicroITS: A scaled-down ITS platform. In: Lecture Notes in Computer Science: . Paper presented at 8th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2018 and 14th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2018, held in conjunction with ESWeek 2018; Turin; Italy; 4 October 2018 through 5 October 2018 (pp. 214-221). Springer
Open this publication in new window or tab >>MicroITS: A scaled-down ITS platform
2019 (English)In: Lecture Notes in Computer Science, Springer, 2019, p. 214-221Conference paper, Published paper (Refereed)
Abstract [en]

Intelligent Transportation Systems (ITS) are an excellent illustration of the types of challenges that future technologists must address. In previous work we presented a course designed to engage students with theoretical aspects of embedded and cyber-physical systems. In this paper we present MicroITS, a platform addressing applied aspects. We articulate the design goals that we believe are needed to achieve engagement in an educational setting, and describe the platform and its baseline functionality. We briefly describe example projects that can be realized using MicroITS. Our hope is that this report will encourage the development of a community of educators and students interested in the use and the continued development of the platform. © Springer Nature Switzerland AG 2019.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11615
Keywords
Cyber Physical System, Education computing, Intelligent systems, Intelligent vehicle highway systems, Students, Design goal, Educational settings, Intelligent transportation systems, Theoretical aspects, Embedded systems
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:hh:diva-41548 (URN)10.1007/978-3-030-23703-5_13 (DOI)2-s2.0-85069196047 (Scopus ID)9783030237028 (ISBN)
Conference
8th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2018 and 14th International Workshop on Embedded and Cyber-Physical Systems Education, WESE 2018, held in conjunction with ESWeek 2018; Turin; Italy; 4 October 2018 through 5 October 2018
Funder
Knowledge Foundation
Available from: 2020-02-03 Created: 2020-02-03 Last updated: 2020-02-03Bibliographically approved
Moggi, E., Amin, F. & Taha, W. (2019). System Analysis and Robustness. In: Tiziana Margaria, Susanne Graf & Kim G. Larsen (Ed.), Tiziana Margaria, Susanne Graf & Kim G. Larsen (Ed.), Models, Mindsets, Meta: The What, the How, and the Why Not? Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday (pp. 36-44). Cham: Springer
Open this publication in new window or tab >>System Analysis and Robustness
2019 (English)In: Models, Mindsets, Meta: The What, the How, and the Why Not? Essays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday / [ed] Tiziana Margaria, Susanne Graf & Kim G. Larsen, Cham: Springer, 2019, p. 36-44Chapter in book (Refereed)
Abstract [en]

Software is increasingly embedded in a variety of physical contexts. This imposes new requirements on tools that support the design and analysis of systems. For instance, modeling embedded and cyber-physical systems needs to blend discrete mathematics, which is suitable for modeling digital components, with continuous mathematics, used for modeling physical components. This blending of continuous and discrete creates challenges that are absent when the discrete or the continuous setting are considered in isolation. We consider robustness, that is, the ability of an analysis of a model to cope with small amounts of imprecision in the model. Formally, we identify analyses with monotonic maps between complete lattices (a mathematical framework used for abstract interpretation and static analysis) and define robustness for monotonic maps between complete lattices of closed subsets of a metric space. © Springer Nature Switzerland AG 2019

Place, publisher, year, edition, pages
Cham: Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11200
Keywords
Modeling, Simulation, Hybrid Systems, Cyber-Physical Systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-41304 (URN)10.1007/978-3-030-22348-9_4 (DOI)2-s2.0-85067949429 (Scopus ID)978-3-030-22347-2 (ISBN)978-3-030-22348-9 (ISBN)
Note

Also part of the Theoretical Computer Science and General Issues book sub series (LNTCS, volume 11200)

Available from: 2019-12-24 Created: 2019-12-24 Last updated: 2020-01-24Bibliographically approved
Moggi, E., Farjudian, A. & Taha, W. (2019). System analysis and robustness. In: CEUR Workshop Proceedings: Volume 2504. Paper presented at 20th Italian Conference on Theoretical Computer Science, ICTCS 2019, 9 September 2019 through 11 September 2019 (pp. 1-7). CEUR-WS
Open this publication in new window or tab >>System analysis and robustness
2019 (English)In: CEUR Workshop Proceedings: Volume 2504, CEUR-WS , 2019, p. 1-7Conference paper, Published paper (Refereed)
Abstract [en]

Software is increasingly embedded in a variety of physical contexts. This imposes new requirements on tools that support the design and analysis of systems. For instance, modeling embedded and cyberphysical systems needs to blend discrete mathematics, which is suitable for modeling digital components, with continuous mathematics, used for modeling physical components. This blending of continuous and discrete creates challenges that are absent when the discrete or the continuous setting are considered in isolation. We consider robustness, that is, the ability of an analysis of a model to cope with small amounts of imprecision in the model. Formally, we identify analyses with monotonic maps between complete lattices (a mathematical framework used for abstract interpretation and static analysis) and define robustness for monotonic maps between complete lattices of closed subsets of a metric space. Copyright © 2019 for this paper by its authors.

Place, publisher, year, edition, pages
CEUR-WS, 2019
Series
CEUR Workshop Proceedings, ISSN 1613-0073 ; 2504
Keywords
Analyses, Domain theory, Robustness, Blending, Robustness (control systems), Static analysis, Abstract interpretations, Cyber physical systems (CPSs), Design and analysis, Discrete mathematics, Mathematical frameworks, Physical components, Embedded systems
National Category
Embedded Systems Computer Systems
Identifiers
urn:nbn:se:hh:diva-41543 (URN)2-s2.0-85076003651 (Scopus ID)
Conference
20th Italian Conference on Theoretical Computer Science, ICTCS 2019, 9 September 2019 through 11 September 2019
Available from: 2020-02-04 Created: 2020-02-04 Last updated: 2020-02-04Bibliographically approved
Duracz, A., Moggi, E., Taha, W. & Lin, Z. (2018). A Semantic Account of Rigorous Simulation. In: Marten LohstrohPatricia DerlerMarjan Sirjani (Ed.), Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday (pp. 223-239). Amsterdam: Springer Berlin/Heidelberg, 10760
Open this publication in new window or tab >>A Semantic Account of Rigorous Simulation
2018 (English)In: Principles of Modeling: Essays Dedicated to Edward A. Lee on the Occasion of His 60th Birthday / [ed] Marten LohstrohPatricia DerlerMarjan Sirjani, Amsterdam: Springer Berlin/Heidelberg, 2018, Vol. 10760, p. 223-239Chapter in book (Refereed)
Abstract [en]

Hybrid systems are a powerful formalism for modeling cyber-physical systems. Reachability analysis is a general method for checking safety properties, especially in the presence of uncertainty and non-determinism. Rigorous simulation is a convenient tool for reachability analysis of hybrid systems. However, to serve as proof tool, a rigorous simulator must be correct w.r.t. a clearly defined notion of reachability, which captures what is intuitively reachable in finite time. As a step towards addressing this challenge, this paper presents a rigorous simulator in the form of an operational semantics and a specification in the form of a denotational semantics. We show that, under certain conditions about the representation of enclosures, the rigorous simulator is correct. We also show that finding a representation satisfying these assumptions is non-trivial. © 2018, Springer International Publishing AG, part of Springer Nature.

Place, publisher, year, edition, pages
Amsterdam: Springer Berlin/Heidelberg, 2018
Series
Lecture Notes In Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10760
Keywords
Correctness, Programming languages, Reachability analysis, Computer programming languages, Embedded systems, Hybrid systems, Semantics, Simulators, Denotational semantics, General method, Non Determinism, Operational semantics, Rigorous simulation, Safety property, Uncertainty analysis
National Category
Computer Systems Embedded Systems
Identifiers
urn:nbn:se:hh:diva-38736 (URN)10.1007/978-3-319-95246-8_13 (DOI)2-s2.0-85052713247 (Scopus ID)978-3-319-95245-1 (ISBN)978-3-319-95246-8 (ISBN)
Available from: 2019-01-09 Created: 2019-01-09 Last updated: 2019-01-09Bibliographically approved
Taha, W. (2018). Rigorous simulation. In: Salem, A., Abbas, H. M., Elkharashi, M. W., Eldin, A. M. B., Taher, M., Zaki, A. M. (Ed.), : . Paper presented at 13th International Conference on Computer Engineering and Systems (ICCES 2018) (pp. XXIII-XXIV). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Rigorous simulation
2018 (English)In: / [ed] Salem, A., Abbas, H. M., Elkharashi, M. W., Eldin, A. M. B., Taher, M., Zaki, A. M., Institute of Electrical and Electronics Engineers (IEEE), 2018, p. XXIII-XXIVConference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2018
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-41503 (URN)000465792300002 ()
Conference
13th International Conference on Computer Engineering and Systems (ICCES 2018)
Available from: 2020-02-03 Created: 2020-02-03 Last updated: 2020-02-03Bibliographically approved
Moggi, E., Farjudian, A., Duracz, A. & Taha, W. (2018). Safe & robust reachability analysis of hybrid systems. Theoretical Computer Science, 747, 75-99
Open this publication in new window or tab >>Safe & robust reachability analysis of hybrid systems
2018 (English)In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 747, p. 75-99Article in journal (Refereed) Published
Abstract [en]

Hybrid systems—more precisely, their mathematical models—can exhibit behaviors, like Zeno behaviors, that are absent in purely discrete or purely continuous systems. First, we observe that, in this context, the usual definition of reachability—namely, the reflexive and transitive closure of a transition relation—can be unsafe, i.e., it may compute a proper subset of the set of states reachable in finite time from a set of initial states. Therefore, we propose safe reachability, which always computes a superset of the set of reachable states. Second, in safety analysis of hybrid and continuous systems, it is important to ensure that a reachability analysis is also robust w.r.t. small perturbations to the set of initial states and to the system itself, since discrepancies between a system and its mathematical models are unavoidable. We show that, under certain conditions, the best Scott continuous approximation of an analysis A is also its best robust approximation. Finally, we exemplify the gap between the set of reachable states and the supersets computed by safe reachability and its best robust approximation. © 2018 The Authors

Place, publisher, year, edition, pages
Amsterdam: Elsevier, 2018
Keywords
Computational methods, Computer science, Robustness (control systems), Continuous approximations, Domain theory, Reachability, Reachability analysis, Robust approximations, Small perturbations, Transition relations, Transitive closure, Hybrid systems
National Category
Control Engineering Computational Mathematics Embedded Systems
Identifiers
urn:nbn:se:hh:diva-38699 (URN)10.1016/j.tcs.2018.06.020 (DOI)000447571900005 ()2-s2.0-85048949865 (Scopus ID)
Funder
Knowledge FoundationELLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications
Note

Funding: US NSF Grant number: 1736759

Available from: 2019-01-08 Created: 2019-01-08 Last updated: 2019-01-08Bibliographically approved
Zeng, Y., Bartha, F. & Taha, W. (2017). Compile-Time Extensions to Hybrid ODEs. Electronic Proceedings in Theoretical Computer Science, 52-70
Open this publication in new window or tab >>Compile-Time Extensions to Hybrid ODEs
2017 (English)In: Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180, E-ISSN 2075-2180, p. 52-70Article in journal (Refereed) Published
Abstract [en]

Reachability analysis for hybrid systems is an active area of development and has resulted in many promising prototype tools. Most of these tools allow users to express hybrid system as automata with a set of ordinary differential equations (ODEs) associated with each state, as well as rules for transitions between states. Significant effort goes into developing and verifying and correctly implementing those tools. As such, it is desirable to expand the scope of applicability tools of such as far as possible. With this goal, we show how compile-time transformations can be used to extend the basic hybrid ODE formalism traditionally supported in hybrid reachability tools such as SpaceEx or Flow*. The extension supports certain types of partial derivatives and equational constraints. These extensions allow users to express, among other things, the Euler-Lagrangian equation, and to capture practically relevant constraints that arise naturally in mechanical systems. Achieving this level of expressiveness requires using a binding time-analysis (BTA), program differentiation, symbolic Gaussian elimination, and abstract interpretation using interval analysis. Except for BTA, the other components are either readily available or can be easily added to most reachability tools. The paper therefore focuses on presenting both the declarative and algorithmic specifications for the BTA phase, and establishes the soundness of the algorithmic specifications with respect to the declarative one.

Place, publisher, year, edition, pages
Sydney: Open Publishing Association, 2017
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-35613 (URN)10.4204/EPTCS.247.5 (DOI)000405454600006 ()2-s2.0-85019253166 (Scopus ID)
Available from: 2017-11-30 Created: 2017-11-30 Last updated: 2018-01-13Bibliographically approved
Lierler, Y. & Taha, W. (Eds.). (2017). Practical Aspects of Declarative Languages: 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings. Paper presented at 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017. Heidelberg: Springer Publishing Company
Open this publication in new window or tab >>Practical Aspects of Declarative Languages: 19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017, Proceedings
2017 (English)Conference proceedings (editor) (Refereed)
Abstract [en]

The proceedings contain 14 papers. The special focus in this conference is on Practical Aspects of Declarative Languages. The topics include: Eliminating irrelevant non determinism in functional logic programs; canonicalizing high-level constructs in picat; integrating answer set programming with object-oriented languages; extending answer set programs with interpreted functions as first-class citizens; lowering the learning curve for declarative programming; overlapping patterns for property-based testing; Boltzmann samplers for closed simply-typed lambda terms; selection equilibria of higher-order games; principles and prototype implementation; declarative programming of full-fledged musical applications; a domain-specific language for software-defined radio; a declarative DSL for customizing ASCII art and using iterative deepening for probabilistic logic inference. © Copyright 2017 Elsevier B.V., All rights reserved

Place, publisher, year, edition, pages
Heidelberg: Springer Publishing Company, 2017. p. 215
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 10137
National Category
Computer Sciences
Identifiers
urn:nbn:se:hh:diva-36710 (URN)10.1007/978-3-319-51676-9 (DOI)978-3-319-51675-2 (ISBN)978-3-319-51676-9 (ISBN)
Conference
19th International Symposium, PADL 2017, Paris, France, January 16-17, 2017
Note

Scopus-ID: 2-s2.0-85010203601

Available from: 2018-05-01 Created: 2018-05-01 Last updated: 2018-05-02Bibliographically approved
Duracz, A., Bartha, F. Á. & Taha, W. (2016). Accurate Rigorous Simulation Should be Possible for Good Designs. In: Erika Ábrahám & Sergiy Bogomolov (Ed.), Proceedings of the 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR): . Paper presented at 2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’16), Vienna, Austria, April 11, 2016. Piscataway, NJ: IEEE conference proceedings, Article ID 7479376.
Open this publication in new window or tab >>Accurate Rigorous Simulation Should be Possible for Good Designs
2016 (English)In: Proceedings of the 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR) / [ed] Erika Ábrahám & Sergiy Bogomolov, Piscataway, NJ: IEEE conference proceedings, 2016, article id 7479376Conference paper, Published paper (Refereed)
Abstract [en]

The development of Cyber-Physical Systems benefits from better methods and tools to support the simulation and verification of hybrid (continuous/discrete) models. Acumen is an open source testbed for exploring the design space of what rigorous-but-practical next-generation tools can deliver to developers. Central to Acumen is the notion of rigorous simulation. Like verification tools, rigorous simulation is intended to provide guarantees about the behavior of the system. Like traditional simulation tools, it is intended to be intuitive, practical, and scalable. Whether these two goals can be achieved simultaneously is an important, long-term challenge.

This paper proposes a design principle that can play an important role in meeting this challenge. The principle addresses the criticism that accumulating numerical errors is a serious impediment to practical rigorous simulation. It is inspired by a twofold insight: one relating to the nature of systems engineered in the real world, and the other relating to how numerical errors in the simulation of a model can be recast as errors in the state or parameters of the model in the simulation. We present a suite of small, concrete benchmarks that can be used to assess the extent to which a rigorous simulator upholds the proposed principle. We also report on which benchmarks Acumen's current rigorous simulator already succeeds and which ones remain challenging.

Place, publisher, year, edition, pages
Piscataway, NJ: IEEE conference proceedings, 2016
Keywords
modeling, simulation, interval analysis, stability
National Category
Computational Mathematics
Identifiers
urn:nbn:se:hh:diva-30577 (URN)10.1109/SNR.2016.7479376 (DOI)000382758100001 ()2-s2.0-84978544274 (Scopus ID)978-1-5090-3079-8 (ISBN)
Conference
2nd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR’16), Vienna, Austria, April 11, 2016
Funder
Knowledge FoundationVINNOVA, 2011-01819
Note

Funding: US NSF award CPS-1136099, the Swedish Knowledge Foundation (KK), The CERES Center, and VINNOVA (Dnr. 2011-01819).

Available from: 2016-03-23 Created: 2016-03-23 Last updated: 2018-03-22Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0003-3160-9188

Search in DiVA

Show all publications