Zobrazeno 1 - 10
of 17
pro vyhledávání: '"Paul S. Miner"'
Publikováno v:
AIAA Aviation 2019 Forum.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d6df2317c81a45176e09abe4f273e6c7
https://doi.org/10.2514/6.2019-2834
https://doi.org/10.2514/6.2019-2834
Autor:
Paul S. Miner
Publikováno v:
IFAC Proceedings Volumes. 28:31-36
A significant portion of the ANSI/IEEE-854 Standard for Radix-Independent Floating Point Arithmetic is fonnally defined using PVS (Prototype Verification System). Since IEEE-854 is a generalization of the ANSI/IEEE-754 Standard for Binary Floating-Po
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::da5026bff92e452a254026b56efa19ba
https://doi.org/10.1016/s1474-6670(17)44820-8
https://doi.org/10.1016/s1474-6670(17)44820-8
Publikováno v:
2006 ieee/aiaa 25TH Digital Avionics Systems Conference.
Use of unmanned aircraft systems (UASs) has been characterized as the next great step forward in the evolution of civil aviation. Indeed, UASs are in limited civil use in the United States today, and many believe that the time is rapidly approaching
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5e33a5d0ce3f8287dc3f31906b620043
https://doi.org/10.1109/dasc.2006.313735
https://doi.org/10.1109/dasc.2006.313735
Publikováno v:
Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems ISBN: 9783540231677
FORMATS/FTRTFT
FORMATS/FTRTFT
Davies and Wakerly show that Byzantine fault tolerance can be achieved by a cascade of broadcasts and middle value select functions. We present an extension of the Davies and Wakerly protocol, the unified protocol, and its proof of correctness. We pr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6bdcc6325e64ebe40693dac52104f028
https://doi.org/10.1007/978-3-540-30206-3_13
https://doi.org/10.1007/978-3-540-30206-3_13
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540230175
TPHOLs
TPHOLs
Four kinds of abstraction for the design and analysis of fault tolerant distributed systems are discussed. These abstractions concern system messages, faults, fault masking voting, and communication. The abstractions are formalized in higher order lo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b2c09a2f6b32330557a627c60f8a543a
https://doi.org/10.1007/978-3-540-30142-4_19
https://doi.org/10.1007/978-3-540-30142-4_19
Publikováno v:
Proceedings. The 21st Digital Avionics Systems Conference.
The Scalable Processor-Independent Design for Electromagnetic Resilience (SPIDER) is a new family of fault-tolerant architectures under development at NASA Langley Research Center (LaRC). The SPIDER is a general-purpose computational platform suitabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4a52fc00778448b233e4c1b4d94ca1e0
https://doi.org/10.1109/dasc.2002.1053014
https://doi.org/10.1109/dasc.2002.1053014
A prototype fault-tolerant clock synchronization system is designed to a proven correct formal specification. The specification is derived from F.B. Schneider's (1987) general paradigm for Byzantine resilient clock synchronization. One addition to th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::272848fcec835af7eda0374a1b12dd7e
https://zenodo.org/record/1266956
https://zenodo.org/record/1266956
Publikováno v:
SRDS
We propose a design strategy that exploits the strengths of different formal approaches to establish a reliable path from a mechanically verified high-level description to a concrete gate-level realization. We demonstrate the use of this approach in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::18a8bafbf253a59a5044ff424b9b11da
https://doi.org/10.1109/reldis.1994.336902
https://doi.org/10.1109/reldis.1994.336902
Publikováno v:
19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126).
In a joint project with the FAA, NASA Langley is developing a hardware design in accordance with RTCA DO-254: Design Assurance Guidance for Airborne Electronic Hardware. The purpose of the case study is to gain understanding of the new guidance docum
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e9d81b071ff981427efae10d5c228ae8
https://doi.org/10.1109/dasc.2000.886872
https://doi.org/10.1109/dasc.2000.886872
Autor:
Paul S. Miner, Steven D. Johnson
Publikováno v:
Advances in Hardware Design and Verification ISBN: 9781504128858
CHARME
CHARME
Practical applications of formal methods research require the integrated use of distinct tools for reasoning and design. Many approaches to this problem involve embedding specialized verification procedures in a theorem prover or logical framework. I
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7a4d7ad9f84a7641af1b047e01055338
https://doi.org/10.1007/978-0-387-35190-2_17
https://doi.org/10.1007/978-0-387-35190-2_17