Titlebook: NASA Formal Methods; 6th International Sy Julia M. Badger,Kristin Yvonne Rozier Conference proceedings 2014 Springer International Publishi

小步舞

On the Quantum Formalization of Coherent Light in HOL,hereafter, basic quantum states of light, called fock states, are formalized and many theorems are proved over such states, e.g., the effect of the quantum creation operation over fock states. Finally, the fundamental notions of coherent light are formalized and their properties also verified.

ROOF

怕失去钱

DO-333 Certification Case Studies,ement systems. This paper presents three case studies describing the use of different classes of formal methods to satisfy DO-178C certification objectives. The case studies examine different aspects of a common avionics example, a dual-channel Flight Guidance System (FGS), which is representative o

绿州

A Compositional Monitoring Framework for Hard Real-Time Systems,y combined with faults originated by the software and/or hardware. This is particularly important when we have real-time embedded systems made of several components that must combine different levels of criticality, and different levels of correctness requirements. This paper introduces a compositio

小步舞

思想

我说不重要

Distinguishing Sequences for Partially Specified FSMs, FSMs, the computational complexity of constructing Adaptive and Preset DSs (ADSs/PDSs) for PSFSMs has not been addressed. This paper shows that it is possible to check the existence of an ADS in polynomial time but the corresponding problem for PDSs is .. We also report on the results of experiment

HAUNT

On Proving Recoverability of Smart Electrical Grids,g the network through remotely controlled (dis)connectors. The consumers of the grid have typically distinct priorities, e.g., a hospital and an airport have the highest priority and the street lighting has a lower priority. This means that when electricity supply is compromised, e.g., during a stor

FLINT

Intractable

Mechanized, Compositional Verification of Low-Level Code,y established for high-level representations of a system, but also for low-level representations..In this paper, we therefore present a compositional semantics and a related proof calculus for possibly non-deterministic low-level languages. The calculus facilitates total correctness proofs about pro