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

research-article

Open access

Synchronous Programming with Refinement Types

Authors:

José Luiz Vargas de Mendonça,

Bereket Shimels Ayele,

Bereket Ngussie Bekele,

Pranjal Sharma,

Nicholas Wohlfeil,

Jean-Baptiste JeanninAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 8, Issue ICFP

Article No.: 268, Pages 938 - 972

https://doi.org/10.1145/3674657

Published: 15 August 2024 Publication History

Abstract

Cyber-Physical Systems (CPS) consist of software interacting with the physical world, such as robots, vehicles, and industrial processes. CPS are frequently responsible for the safety of lives, property, or the environment, and so software correctness must be determined with a high degree of certainty. To that end, simply testing a CPS is insufficient, as its interactions with the physical world may be difficult to predict, and unsafe conditions may not be immediately obvious. Formal verification can provide stronger safety guarantees but relies on the accuracy of the verified system in representing the real system. Bringing together verification and implementation can be challenging, as languages that are typically used to implement CPS are not easy to formally verify, and languages that lend themselves well to verification often abstract away low-level implementation details. Translation between verification and implementation languages is possible, but requires additional assurances in the translation process and increases software complexity; having both in a single language is desirable. This paper presents a formalization of MARVeLus, a CPS language which combines verification and implementation. We develop a metatheory for its synchronous refinement type system and demonstrate verified synchronous programs executing on real systems.

References

[1]

Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei Hsin Ho. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid Systems, G. Goos, J. Hartmanis, Robert L. Grossman, Anil Nerode, Anders P. Ravn, and Hans Rischel (Eds.). 736, Springer, Berlin, Heidelberg. 209–229. isbn:978-3-540-57318-0 978-3-540-48060-0 https://doi.org/10.1007/3-540-57318-6_30

[2]

Aaron D. Ames, Jessy W. Grizzle, and Paulo Tabuada. 2014. Control barrier function based quadratic programs with application to adaptive cruise control. In 53rd IEEE Conference on Decision and Control (CDC 2014). IEEE, Los Angeles, CA, USA. 6271–6278. isbn:978-1-4673-6090-6 978-1-4799-7746-8 978-1-4799-7745-1 https://doi.org/10.1109/CDC.2014.7040372

[3]

Abhishek Anand and Ross Knepper. 2015. ROSCoq: Robots Powered by Constructive Reals. In Interactive Theorem Proving (ITP 2015), Christian Urban and Xingyuan Zhang (Eds.). 9236, Springer International Publishing, Cham. 34–50. isbn:978-3-319-22101-4 978-3-319-22102-1 https://doi.org/10.1007/978-3-319-22102-1_3

[4]

Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. 2020. Reactive probabilistic programming. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020). Association for Computing Machinery, New York, NY, USA. 898–912. https://doi.org/10.1145/3385412.3386009

Digital Library

[5]

Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer, Maximilian Schwenger, and Christoph Torens. 2020. RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft. In Computer Aided Verification (CAV 2020), Shuvendu K. Lahiri and Chao Wang (Eds.). 12225, Springer International Publishing, Cham. 28–39. isbn:978-3-030-53290-1 978-3-030-53291-8 https://doi.org/10.1007/978-3-030-53291-8_3 Series Title: Lecture Notes in Computer Science

Digital Library

[6]

Albert Benveniste, Timothy Bourke, Benoit Caillaud, Bruno Pagano, and Marc Pouzet. 2014. A type-based analysis of causality loops in hybrid systems modelers. In Proceedings of the 17th international conference on Hybrid systems: computation and control (HSCC 2014). ACM Press, Berlin, Germany. 71–82. isbn:978-1-4503-2732-9 https://doi.org/10.1145/2562059.2562125

Digital Library

[7]

Albert Benveniste, Timothy Bourke, Benoît Caillaud, and Marc Pouzet. 2011. A hybrid synchronous language with hierarchical automata: static typing and translation to synchronous code. In Proceedings of the 9th ACM international conference on Embedded software (EMSOFT 2011). ACM, Taipei, Taiwan. 137–148. isbn:978-1-4503-0714-7 https://doi.org/10.1145/2038642.2038664

Digital Library

[8]

Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. 2018. VeriPhy: verified controller executables from verified cyber-physical system models. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2018). ACM, Philadelphia PA USA. 617–630. isbn:978-1-4503-5698-5 https://doi.org/10.1145/3192366.3192406

Digital Library

[9]

Michael H Borkowski, Niki Vazou, and Ranjit Jhala. 2024. Mechanizing refinement types. Proceedings of the ACM on Programming Languages (POPL 2024), 8 (2024), 2099–2128. https://doi.org/10.1145/3632912

Digital Library

[10]

Sylvain Boulmé and Grégoire Hamon. 2001. Certifying Synchrony for Free. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), G. Goos, J. Hartmanis, J. Van Leeuwen, Robert Nieuwenhuis, and Andrei Voronkov (Eds.). 2250, Springer, Berlin, Heidelberg. 495–506. isbn:978-3-540-42957-9 978-3-540-45653-7 https://doi.org/10.1007/3-540-45653-8_34

[11]

Timothy Bourke, Lélio Brun, Pierre-Evariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. 2017. A Formally Verified Compiler for Lustre. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017), 52, 6 (2017), 586–601. https://doi.org/10.1145/3062341.3062358

Digital Library

[12]

Timothy Bourke and Marc Pouzet. 2013. Zélus: a synchronous language with ODEs. In Proceedings of the 16th international conference on Hybrid systems: computation and control (HSCC 2013). ACM Press, Philadelphia, Pennsylvania, USA. 113. isbn:978-1-4503-1567-8 https://doi.org/10.1145/2461328.2461348

Digital Library

[13]

F. Boussinot and R. de Simone. 1991. The ESTEREL language. Proc. IEEE, 79, 9 (1991), Sept., 1293–1304. issn:00189219 https://doi.org/10.1109/5.97299

[14]

P. Caspi, D. Pilaud, N. Halbwachs, and J. A. Plaice. 1987. LUSTRE: A Declarative Language for Real-Time Programming. In Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 1987). ACM, New York, NY, USA. 178–188. isbn:0897912152 https://doi.org/10.1145/41625.41641

Digital Library

[15]

Paul Caspi and Marc Pouzet. 1996. Synchronous Kahn networks. In Proceedings of the first ACM SIGPLAN international conference on Functional programming (ICFP 1996). ACM Press, Philadelphia, Pennsylvania, United States. 226–238. isbn:978-0-89791-770-4 https://doi.org/10.1145/232627.232651

Digital Library

[16]

Paul Caspi and Marc Pouzet. 1998. A Co-iterative Characterization of Synchronous Stream Functions. Electronic Notes in Theoretical Computer Science, 11 (1998), 1–21. issn:15710661 https://doi.org/10.1016/S1571-0661(04)00050-7

Digital Library

[17]

Adrien Champion, Alain Mebsout, Christoph Sticksel, and Cesare Tinelli. 2016. The Kind 2 Model Checker. In Computer Aided Verification (CAV 2016), Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 510–517. isbn:978-3-319-41540-6 https://doi.org/10.1007/978-3-319-41540-6_29

[18]

Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Shimels Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma, Nicholas Wohlfeil, Yicheng Zhang, and Jean-Baptiste Jeannin. 2024. Synchronous Programming with Refinement Types. https://doi.org/10.48550/arXiv.2406.06221 arXiv:2406.06221 [cs]. Extended version

[19]

Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Shimels Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma, Nicholas Wohlfeil, Yicheng Zhang, and Jean-Baptiste Jeannin. 2024. Synchronous Programming with Refinement Types. https://doi.org/10.5281/zenodo.12702677 Artifact

Digital Library

[20]

Jiawei Chen, José Luiz Vargas de Mendonça, Shayan Jalili, Bereket Ayele, Bereket Ngussie Bekele, Zhemin Qu, Pranjal Sharma, Tigist Shiferaw, Yicheng Zhang, and Jean-Baptiste Jeannin. 2022. Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation. In Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2022). ACM, New York, NY, USA. 68–79. isbn:978-1-4503-9907-4 https://doi.org/10.1145/3563822.3568015

Digital Library

[21]

Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. 2006. Mixing Signals and Modes in Synchronous Data-Flow Systems. In Proceedings of the 6th ACM & IEEE International Conference on Embedded Software (EMSOFT 2006). ACM, New York, NY, USA. 73–82. isbn:1595935428 https://doi.org/10.1145/1176887.1176899

Digital Library

[22]

Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. 2017. SCADE 6: A formal language for embedded critical software development (invited paper). In 2017 International Symposium on Theoretical Aspects of Software Engineering (TASE 2017). IEEE, 1–11. https://doi.org/10.1109/TASE.2017.8285623

[23]

Pascal Cuoq and Marc Pouzet. 2001. Modular causality in a synchronous stream language. In European Symposium on Programming (ESOP 2001), Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, and David Sands (Eds.). 2028, Springer, Berlin, Heidelberg. 237–251. isbn:978-3-540-41862-7 978-3-540-45309-3 https://doi.org/10.1007/3-540-45309-1_16 Series Title: Lecture Notes in Computer Science

[24]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, C. R. Ramakrishnan, and Jakob Rehof (Eds.). 4963, Springer, Berlin, Heidelberg. 337–340. isbn:978-3-540-78799-0 978-3-540-78800-3 https://doi.org/10.1007/978-3-540-78800-3_24

[25]

Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, and Mira Mezini. 2022. Dependently-typed data plane programming. Proceedings of the ACM on Programming Languages, 6, POPL 2022 (2022), 1–28. https://doi.org/10.1145/3498701

Digital Library

[26]

Georgios E Fainekos and George J Pappas. 2009. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410, 42 (2009), 30. https://doi.org/10.1016/j.tcs.2009.06.021

Digital Library

[27]

Spencer P. Florence, Shu-Hung You, Jesse A. Tov, and Robert Bruce Findler. 2019. A Calculus for Esterel: If Can, Can. If No Can, No Can. Proceedings of the ACM on Programming Languages, 3, POPL 2019 (2019), 1–29. https://doi.org/10.1145/3290374

Digital Library

[28]

Khalil Ghorbal and André Platzer. 2014. Characterizing Algebraic Invariants by Differential Radical Invariants. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Erika Ábrahám and Klaus Havelund (Eds.). 8413, Springer, Berlin, Heidelberg. 279–294. isbn:978-3-642-54861-1 978-3-642-54862-8 https://doi.org/10.1007/978-3-642-54862-8_19 Series Title: Lecture Notes in Computer Science

[29]

Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, and Sayan Mitra. 2020. Koord: A Language for Programming and Verifying Distributed Robotics Application. Proceedings of the ACM on Programming Languages, 4, OOPSLA 2020 (2020), Article 232, 30 pages. https://doi.org/10.1145/3428300

Digital Library

[30]

Ritwika Ghosh, Joao P. Jansch-Porto, Chiao Hsieh, Amelia Gosse, Minghao Jiang, Hebron Taylor, Peter Du, Sayan Mitra, and Geir Dullerud. 2020. CyPhyHouse: A programming, simulation, and deployment toolchain for heterogeneous distributed coordination. In IEEE International Conference on Robotics and Automation (ICRA 2020). IEEE, 6654–6660. https://doi.org/10.1109/ICRA40945.2020.9196513

[31]

George Hagen and Cesare Tinelli. 2008. Scaling Up the Formal Verification of Lustre Programs with SMT-Based Techniques. In Formal Methods in Computer-Aided Design (FMCAD 2008). IEEE, 1–9. https://doi.org/10.1109/FMCAD.2008.ECP.19

[32]

N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The synchronous data flow programming language LUSTRE. Proc. IEEE, 79, 9 (1991), Sept., 1305–1320. issn:00189219 https://doi.org/10.1109/5.97300

[33]

Jean-Baptiste Jeannin and André Platzer. 2014. dTL^2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. In Automated Reasoning: 7th International Joint Conference (IJCAR 2014), Held as Part of the Vienna Summer of Logic (VSL 2014), Stéphane Demri, Deepak Kapur, and Christoph Weidenbach (Eds.). 8562, Springer International Publishing, Cham. 292–306. isbn:978-3-319-08586-9 978-3-319-08587-6 https://doi.org/10.1007/978-3-319-08587-6_22 Series Title: Lecture Notes in Computer Science

[34]

Ranjit Jhala and Niki Vazou. 2021. Refinement types: A tutorial. Foundations and Trends® in Programming Languages, 6, 3–4 (2021), 159–317. https://doi.org/10.1561/2500000032

[35]

Eduard Kamburjan. 2021. From post-conditions to post-region invariants: deductive verification of hybrid objects. In Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (HSCC 2021). ACM, Nashville Tennessee. 1–11. isbn:978-1-4503-8339-4 https://doi.org/10.1145/3447928.3456633

Digital Library

[36]

Sarah M. Loos, André Platzer, and Ligia Nistor. 2011. Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In Formal Methods (FM 2011), Michael Butler and Wolfram Schulte (Eds.). 6664, Springer, Berlin, Heidelberg. 42–56. isbn:978-3-642-21436-3 978-3-642-21437-0 https://doi.org/10.1007/978-3-642-21437-0_6 Series Title: Lecture Notes in Computer Science

[37]

Gregory Malecha, Daniel Ricketts, Mario M. Alvarez, and Sorin Lerner. 2016. Towards foundational verification of cyber-physical systems. In Science of Security for Cyber-Physical Systems Workshop (SOSCYPS 2016). IEEE, 1–5. https://doi.org/10.1109/SOSCYPS.2016.7580000

[38]

Zohar Manna and Amir Pnueli. 1992. The Temporal Logic of Reactive and Concurrent Systems. Springer New York, New York, NY. isbn:978-1-4612-6950-2 978-1-4612-0931-7 https://doi.org/10.1007/978-1-4612-0931-7

[39]

Aakar Mehra, Wen-Loong Ma, Forrest Berg, Paulo Tabuada, Jessy W. Grizzle, and Aaron D. Ames. 2015. Adaptive cruise control: Experimental validation of advanced controllers on scale-model cars. In American Control Conference (ACC 2015). IEEE, Chicago, IL, USA. 1411–1418. isbn:978-1-4799-8684-2 https://doi.org/10.1109/ACC.2015.7170931

[40]

Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic typing with dependent types. In Exploring New Frontiers of Theoretical Informatics: IFIP 18th World Computer Congress TC1 3rd International Conference on Theoretical Computer Science (TCS 2004). Springer, Boston, MA. 437–450. https://doi.org/10.1007/1-4020-8141-3_34

[41]

Ioannis Parissis. 1996. Test de logiciels synchrones spécifiés en Lustre. Ph. D. Dissertation. Université Joseph-Fourier-Grenoble I. https://theses.hal.science/tel-00005010v1/document

[42]

Benjamin C. Pierce. 2005. Advanced topics in types and programming languages. MIT press. issn:0010-4620 https://doi.org/10.1093/comjnl/bxh138

[43]

André Platzer. 2008. Differential Dynamic Logic for Hybrid Systems. Journal of Automated Reasoning, 41, 2 (2008), Aug., 143–189. issn:0168-7433, 1573-0670 https://doi.org/10.1007/s10817-008-9103-8

Digital Library

[44]

André Platzer. 2018. Logical Foundations of Cyber-Physical Systems. Springer International Publishing, Cham. isbn:978-3-319-63587-3 978-3-319-63588-0 https://doi.org/10.1007/978-3-319-63588-0

[45]

Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). IEEE, 46–57. https://doi.org/10.1109/SFCS.1977.32 ISSN: 0272-5428

Digital Library

[46]

Stephen Prajna and Ali Jadbabaie. 2004. Safety Verification of Hybrid Systems Using Barrier Certificates. In Hybrid Systems: Computation and Control (HSCC 2004), Rajeev Alur and George J. Pappas (Eds.). Springer, Berlin, Heidelberg. 477–492. isbn:978-3-540-24743-2 https://doi.org/10.1007/978-3-540-24743-2_32

[47]

Christophe Ratel. 1992. Définition et Réalisation d’un Outil de Vérification Formelle de Programmes LUSTRE: le Système LESAR. Ph. D. Dissertation. Université Joseph Fourier. https://tel.archives-ouvertes.fr/file/index/docid/341223/filename/Ratel.Christophe_1992_these.pdf

[48]

Patrick M. Rondon, Ming Kawaguci, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation (PLDI 2008). ACM Press, Tucson, AZ, USA. 159. isbn:978-1-59593-860-2 https://doi.org/10.1145/1375581.1375602

Digital Library

[49]

Astrid Rupp, Markus Tranninger, Raffael Wallner, Jasmina Zubača, Martin Steinberger, and Martin Horn. 2019. Fast and low-cost testing of advanced driver assistance systems using small-scale vehicles. IFAC-PapersOnLine, 52, 5 (2019), 34–39. https://doi.org/10.1016/j.ifacol.2019.09.006

[50]

CG Rusu, IT Birou, and E Szöke. 2010. Fuzzy based obstacle avoidance system for autonomous mobile robot. In IEEE International Conference on Automation, Quality and Testing, Robotics (AQTR 2010). 1, IEEE, 1–6. https://doi.org/10.1109/AQTR.2010.5520862

Digital Library

[51]

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, and Santiago Zanella-Béguelin. 2016. Dependent Types and Multi-Monadic Effects in F*. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016). ACM, New York, NY, USA. 256–270. isbn:9781450335492 https://doi.org/10.1145/2837614.2837655

Digital Library

[52]

Alfred Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. In Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, 24–84. https://doi.org/10.1007/978-3-7091-9459-1_3

[53]

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (ICFP 2014). ACM, New York, NY, USA. 269–282. isbn:978-1-4503-2873-9 https://doi.org/10.1145/2628136.2628161

Digital Library

[54]

Shuhuan Wen, Wei Zheng, Jinghai Zhu, Xiaoli Li, and Shengyong Chen. 2011. Elman fuzzy adaptive control for obstacle avoidance of mobile robots using hybrid force/position incorporation. IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), 42, 4 (2011), 603–608. https://doi.org/10.1109/TSMCC.2011.2157682

Digital Library

[55]

A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), Nov., 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093

Digital Library

Cited By

Kuwar VSrivastava YGaur SYadav ABhide PUpreti S(2024)Enhancing User Experiences in Cyber-Physical Systems for Real-Time Feedback and Intelligent AutomationNavigating Cyber-Physical Systems With Cutting-Edge Technologies10.4018/979-8-3693-5728-6.ch008(215-234)Online publication date: 22-Nov-2024
https://doi.org/10.4018/979-8-3693-5728-6.ch008

Index Terms

Synchronous Programming with Refinement Types

Recommendations

Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation
FTSCS 2022: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems

Robots and other cyber-physical systems are held to high standards of safety and reliability, and thus one must be confident in the correctness of their software. Formal verification can provide such confidence, but programming languages that lend ...
Program synthesis from polymorphic refinement types
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

We present a method for synthesizing recursive functions that provably satisfy a given specification in the form of a polymorphic refinement type. We observe that such specifications are particularly suitable for program synthesis for two reasons. ...
Correctness-by-Construction Meets Refinement Types
FTfJP 2023: Proceedings of the 25th ACM International Workshop on Formal Techniques for Java-like Programs

Type systems provide specifications and enable reasoning about the programs. Among other benefits, type systems provide guarantees of the absence of certain (ill-typed) program behaviors. Refinement types further enrich the expressiveness of type ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 8, Issue ICFP

August 2024

1031 pages

EISSN:2475-1421

DOI:10.1145/3554318

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2024 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 15 August 2024

Published in PACMPL Volume 8, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
159
Total Downloads

Downloads (Last 12 months)159
Downloads (Last 6 weeks)45

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kuwar VSrivastava YGaur SYadav ABhide PUpreti S(2024)Enhancing User Experiences in Cyber-Physical Systems for Real-Time Feedback and Intelligent AutomationNavigating Cyber-Physical Systems With Cutting-Edge Technologies10.4018/979-8-3693-5728-6.ch008(215-234)Online publication date: 22-Nov-2024
https://doi.org/10.4018/979-8-3693-5728-6.ch008

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents