More Web Proxy on the site http://driver.im/

research-article

A logic-based modeling and verification of CPS

Authors:

Neda Saeedloei,

Gopal GuptaAuthors Info & Claims

ACM SIGBED Review, Volume 8, Issue 2

Pages 31 - 34

https://doi.org/10.1145/2000367.2000374

Published: 01 June 2011 Publication History

Abstract

Cyber-physical systems (CPS) consist of perpetually and concurrently executing physical and computational components. The presence of physical components require the computational components to deal with continuous quantities. A formalism that can model discrete and continuous quantities together with concurrent, perpetual execution is lacking. In this paper we report on the development of a formalism based on logic programming extended with co-induction, constraints over reals, and coroutining that allows CPS to be elegantly modeled. This logic programming realization can be used for verifying interesting properties as well as generating implementations of CPS. We illustrate this formalism by applying it to elegant modeling of the reactor temperature control system. Interesting properties of the system can be verified merely by posing appropriate queries to this model. Precise parametric analysis can also be performed.

References

[1]

R. Alur and D. L. Dill. A theory of timed automata. TCS, 126(2):183--235, 1994.

Digital Library

[2]

R.-J. B. Cristina and C. Cerschi. Modeling and verifying a temperature control system using continuous action systems. In Proc. of the 5th Int. Workshop on FMICS, 2000.

[3]

M. Falaschi and A. Villanueva. Automatic verification of timed concurrent constraint programs. TPLP, 6(3):265--300, 2006.

Digital Library

[4]

Gopal Gupta et al. Coinductive logic programming and its applications. In ICLP, pages 27--44, 2007.

Digital Library

[5]

R. Gupta. Programming models and methods for spatiotemporal actions and reasoning in cyber-physical systems. In NSF Workshop on CPS, 2006.

[6]

T. A. Henzinger and P. hsin Ho. Hytech: The cornell hybrid technology tool. In Hybrid Systems II, LNCS 999, pages 265--293. Springer, 1995.

Digital Library

[7]

J. Jaffar and M. J. Maher. Constraint logic programming: A survey. J. Log. Program., 19/20:503--581, 1994.

[8]

E. A. Lee. Cyber-physical systems: Design challenges. In ISORC, May 2008.

Digital Library

[9]

J. W. Lloyd. Foundations of logic programming/J.W. Lloyd. Springer-Verlag, Berlin, New York, 2nd, extended ed. edition, 1987.

Digital Library

[10]

R. A. Thacker et al. Automatic abstraction for verification of cyber-physical systems. In ICCPS, pages 12--21, 2010.

Digital Library

[11]

R. Alur et al. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, pages 209--229, 1992.

Digital Library

[12]

R. Alur et al. The algorithmic analysis of hybrid systems. TCS, 138:3--34, 1995.

Digital Library

[13]

N. Saeedloei and G. Gupta. A logic based model for the reactor temperature control system. http://www.utdallas.edu/nxs048000/reactor.pdf.

[14]

N. Saeedloei and G. Gupta. Timed definite clause omega-grammars. In ICLP (Technical Communications), pages 212--221, 2010.

[15]

N. Saeedloei and G. Gupta. Verifying complex continuous real-time systems with coinductive CLP(R). In LATA, pages 536--548, 2010.

Digital Library

[16]

V. A. Saraswat, R. Jagadeesan, and V. Gupta. Foundations of timed concurrent constraint programming. In LICS, pages 71--80, 1994.

[17]

L. Simon, A. Bansal, A. Mallya, and G. Gupta. Co-logic programming: Extending logic programming with coinduction. In ICALP, pages 472--483, 2007.

Digital Library

[18]

L. Sterling and E. Shapiro. The art of Prolog (2nd ed.): advanced programming techniques. MIT Press, Cambridge, MA, USA, 1994.

Digital Library

[19]

X. Nicollin et al. An approach to the description and analysis of hybrid systems. In Hybrid Systems, pages 149--178, 1992.

Digital Library

Cited By

Varanasi SArias JSalazar ELi FBasu KGupta G(2022)Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)Practical Aspects of Declarative Languages10.1007/978-3-030-94479-7_12(181-190)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-94479-7_12
Wang Y(2021)Design of Trustworthy Cyber–Physical–Social Systems With Discrete Bayesian OptimizationJournal of Mechanical Design10.1115/1.4049532143:7Online publication date: 5-Feb-2021
https://doi.org/10.1115/1.4049532
Wang Y(2021)Topology-informed information dynamics modeling in cyber–physical–social system networksArtificial Intelligence for Engineering Design, Analysis and Manufacturing10.1017/S0890060421000159(1-16)Online publication date: 14-Jul-2021
https://doi.org/10.1017/S0890060421000159
Show More Cited By

Index Terms

A logic-based modeling and verification of CPS
1. Computer systems organization
  1. Embedded and cyber-physical systems
  2. Real-time systems
2. Computing methodologies
  1. Modeling and simulation
    1. Model development and analysis
      1. Model verification and validation

Recommendations

CPS: Role, Characteristics, Architectures and Future Potentials
Abstract
CPS entails the incorporation of four key characteristic technologies. CPS device technologies, CPS computational technologies, Cyber Physical System of Systems (CPSoS) and CPS networking and communication (CPS-ComNet) technologies. Multiple CPS ...
Towards CPS Verification Engineering
iiWAS '20: Proceedings of the 22nd International Conference on Information Integration and Web-based Applications & Services

While formal verification techniques are inevitable to ensure safety of critical cyber-phyical systems (CPS), engineering techniques to support the design and analysis of such CPS are still in their infancy. Therefore, we take a first step towards the ...
Mechanized Verification of CPS Transformations
Logic for Programming, Artificial Intelligence, and Reasoning
Abstract
Transformation to continuation-passing style (CPS) is often performed by optimizing compilers for functional programming languages. As part of the development and proof of correctness of a compiler for the mini-ML functional language, we have ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGBED Review

ACM SIGBED Review Volume 8, Issue 2

Work-in-Progress (WiP) Session of the 2nd International Conference on Cyber Physical Systems

June 2011

41 pages

EISSN:1551-3688

DOI:10.1145/2000367

Issue’s Table of Contents

Copyright © 2011 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 June 2011

Published in SIGBED Volume 8, Issue 2

Check for updates

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
163
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Varanasi SArias JSalazar ELi FBasu KGupta G(2022)Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)Practical Aspects of Declarative Languages10.1007/978-3-030-94479-7_12(181-190)Online publication date: 17-Jan-2022
https://dl.acm.org/doi/10.1007/978-3-030-94479-7_12
Wang Y(2021)Design of Trustworthy Cyber–Physical–Social Systems With Discrete Bayesian OptimizationJournal of Mechanical Design10.1115/1.4049532143:7Online publication date: 5-Feb-2021
https://doi.org/10.1115/1.4049532
Wang Y(2021)Topology-informed information dynamics modeling in cyber–physical–social system networksArtificial Intelligence for Engineering Design, Analysis and Manufacturing10.1017/S0890060421000159(1-16)Online publication date: 14-Jul-2021
https://doi.org/10.1017/S0890060421000159
Huang CWang DChawla N(2020)Scalable Uncertainty-Aware Truth Discovery in Big Data Social Sensing Applications for Cyber-Physical SystemsIEEE Transactions on Big Data10.1109/TBDATA.2017.26693086:4(702-713)Online publication date: 1-Dec-2020
https://doi.org/10.1109/TBDATA.2017.2669308
Morozov DLezoche MPanetto H(2018)Multi-paradigm modelling of Cyber-Physical SystemsIFAC-PapersOnLine10.1016/j.ifacol.2018.08.33451:11(1385-1390)Online publication date: 2018
https://doi.org/10.1016/j.ifacol.2018.08.334
Letichevsky ALetychevskyi OSkobelev VVolkov V(2017)Cyber-Physical SystemsCybernetics and Systems Analysis10.5555/3169141.316917853:6(821-834)Online publication date: 1-Nov-2017
https://dl.acm.org/doi/10.5555/3169141.3169178
Farzaneh MKugele SKnoll A(2017)A graphical modeling tool supporting automated schedule synthesis for time-sensitive networking2017 22nd IEEE International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA.2017.8247599(1-8)Online publication date: 12-Sep-2017
https://dl.acm.org/doi/10.1109/ETFA.2017.8247599
Letichevsky ALetychevskyi OSkobelev VVolkov V(2017)Cyber-Physical SystemsCybernetics and Systems Analysis10.1007/s10559-017-9984-953:6(821-834)Online publication date: 23-Nov-2017
https://doi.org/10.1007/s10559-017-9984-9
Liu CChen FZhu JZhang ZZhang CZhao CWang T(2017)Characteristic, Architecture, Technology, and Design Methodology of Cyber-Physical SystemsIndustrial IoT Technologies and Applications10.1007/978-3-319-60753-5_25(230-246)Online publication date: 19-Aug-2017
https://doi.org/10.1007/978-3-319-60753-5_25
Saeedloei NGupta G(2016)A methodology for modeling and verification of cyber-physical systems based on logic programmingACM SIGBED Review10.1145/2930957.293096313:2(34-42)Online publication date: 27-Apr-2016
https://dl.acm.org/doi/10.1145/2930957.2930963
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents