Imagen de Portada
Código QR

Model Checking: Algorithmic Verification and Debugging.

The authors discuss their formulation of the process of model checking and its historical background. Mathematical logic is used in model checking to confirm that computer program behavior conforms to the correct specifications. While the Floyd-Hoare style deductive verification method was used sinc...

Descripción completa

Publicado en:Communications of the ACM Vol. 52; no. 11; pp. 75 - 85
Autores principales: Clarke, Edmund M., Emerson, E. Allen, Sifakis, Joseph
Formato: Artículo
Publicado: Association for Computing Machinery Nov2009
Materias:
Software verification
Computer software correctness
Technical specifications
Philosophy of mathematics
Debugging
Computer software testing
History
Acceso en línea:Ver este registro en EBSCOhost
Sumario:The authors discuss their formulation of the process of model checking and its historical background. Mathematical logic is used in model checking to confirm that computer program behavior conforms to the correct specifications. While the Floyd-Hoare style deductive verification method was used since the 1960s, it was not useful for large programs. Model checking was devised using temporal logic (TL) that describes change over time. Debugging, correctness, expressiveness, efficiency and accounting for architectures and their features in model checking are detailed.