caa a22 4500 475797639 CHVBK 20180406123729.0 cr unu---uuuuu 170329e20001001xx s 000 0 eng 10.1023/A:1008713601998 doi (NATIONALLICENCE)springer-10.1023/A:1008713601998 Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System [Elektronische Daten] [Sérgio Campos, Edmund Clarke, Orna Grumberg] In this work we propose a verification methodology consisting of selective quantitative timing analysis and interval model checking. Our methods can aid not only in determining if a system works correctly, but also in understanding how well the system works. The selective quantitative algorithms compute minimum and maximum delays over a selected subset of system executions. A linear-time temporal logic (LTL) formula is used to select either infinite paths or finite intervals over which the computation is performed. We show how tableau for LTL formulas can be used for selecting either paths or intervals and also for model checking formulas interpreted over paths or intervals. To demonstrate the usefulness of our methods we have verified a complex and realistic distributed real-time system. Our tool has been able to analyze the system and to compute the response time of the various components. Moreover, we have been able to identify inefficiencies that caused the response time to increase significantly (about 50%). After changing the design we not only verified that the response time was lower, but were also able to determine the causes for the poor performance of the original model using interval model checking. Kluwer Academic Publishers, 2000 symbolic model checking nationallicence temporal logic model checking nationallicence LTL model checking nationallicence quantitative timing analysis nationallicence real-time systems nationallicence Campos Sérgio Dept. Ciência da Computação, Univ. Federal de Minas Gerais, 31270, Belo Horizonte, MG, Brasil aut Clarke Edmund School of Computer Science, Carnegie Mellon University, 15213, Pittsburgh, PA, USA aut Grumberg Orna Department of Computer Science, The Technion, 32000, Haifa, Israel aut Formal Methods in System Design Kluwer Academic Publishers 17/2(2000-10-01), 163-192 0925-9856 17:2<163 2000 17 10703 https://doi.org/10.1023/A:1008713601998 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008713601998 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Campos Sérgio Dept. Ciência da Computação, Univ. Federal de Minas Gerais, 31270, Belo Horizonte, MG, Brasil aut NATIONALLICENCE 700 1- Clarke Edmund School of Computer Science, Carnegie Mellon University, 15213, Pittsburgh, PA, USA aut NATIONALLICENCE 700 1- Grumberg Orna Department of Computer Science, The Technion, 32000, Haifa, Israel aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 17/2(2000-10-01), 163-192 0925-9856 17:2<163 2000 17 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer