Zobrazeno 1 - 10
of 29
pro vyhledávání: '"Geoffrey C. Hulette"'
Autor:
Samuel D. Pollard, Robert C. Armstrong, John Bender, Geoffrey C. Hulette, Raheel S. Mahmood, Karla Morris, Blake C. Rawlings, Jon M. Aytac
Publikováno v:
Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems.
Autor:
Michael Butler, Geoffrey C. Hulette, Thai Son Hoang, Colin Snook, Karla Morris, Robert C. Armstrong
Publikováno v:
Rigorous State-Based Methods
Rigorous State-Based Methods ISBN: 9783030480769
ABZ
Rigorous State-Based Methods ISBN: 9783030480769
ABZ
Statechart notations with ‘run to completion’ semantics, are popular with engineers for designing controllers that respond to events in the environment with a sequence of state transitions. However, they lack formal refinement and rigorous verifi
TLA is a popular temporal logic for writing stuttering-invariant specifications of digital systems. However, TLA lacks higher-order features useful for specifying modern software written in higher-order programming languages. We use categorical techn
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b2bbcaf5e1b7621aa8dd899e2b14a51e
Autor:
Michael Butler, Geoffrey C. Hulette, Colin Snook, Robert C. Armstrong, Thai Son Hoang, Karla Morris
Publikováno v:
Communications in Computer and Information Science ISBN: 9783030591540
Although popular in industry, state-chart notations with ‘run to completion’ semantics lack formal refinement and rigorous verification methods. State-chart models are typically used to design complex control systems that respond to environmental
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0bd79f66e6baa2fd5e33a3d9b29b2374
https://doi.org/10.1007/978-3-030-59155-7_24
https://doi.org/10.1007/978-3-030-59155-7_24
Publikováno v:
Electronic Notes in Theoretical Computer Science. 317:71-83
This work outlines an equation-based formulation of a digital control program and transducer interacting with a continuous physical process, and an approach using the Coq theorem prover for verifying the performance of the combined hybrid system. Con
Publikováno v:
Cyber-Physical Systems Security ISBN: 9783319989341
Cyber-Physical Systems Security
Cyber-Physical Systems Security
Modern digital hardware and software designs are increasingly complex but are themselves only idealizations of a real system that is instantiated in, and interacts with, an analog physical environment. Insights from physics, formal methods, and compl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b5c3c5eb7c24b4de944c483ced3fbaf5
https://doi.org/10.1007/978-3-319-98935-8_1
https://doi.org/10.1007/978-3-319-98935-8_1
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319459424
FMICS-AVoCS
FMICS-AVoCS
Sandia engineers use the Temporal Logic of Actions (TLA) early in the design process for digital systems where safety considerations are critical. TLA allows us to easily build models of interactive systems and prove (in the mathematical sense) that
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2f171bd08aa4e70e395593211c81875a
https://doi.org/10.1007/978-3-319-45943-1_14
https://doi.org/10.1007/978-3-319-45943-1_14
Publikováno v:
Communications in Computer and Information Science ISBN: 9783319295091
FTSCS
FTSCS
Digital systems in an out-of-nominal environment (e.g., one causing hardware bit flips) may not be expected to function correctly in all respects but may be required to fail safely. We present an approach for understanding and verifying a system’s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8adf1c75bba6c9758b2af3274d980707
https://doi.org/10.1007/978-3-319-29510-7_10
https://doi.org/10.1007/978-3-319-29510-7_10
Publikováno v:
GPCE
Twig is a language for writing typemaps , programs which transform the type of a value while preserving its underlying meaning. Typemaps are typically used by tools that generate code, such as multi-language wrapper generators, to automatically conve