LEADER 01039nam0-22002891i-450- 001 990000608900403321 005 20001010 035 $a000060890 035 $aFED01000060890 035 $a(Aleph)000060890FED01 035 $a000060890 100 $a20001010d--------km-y0itay50------ba 101 0 $aita 105 $ay-------001yy 200 1 $aSULL'EVOLUZIONE DEL DANNEGGIAMENTO PER MICROFESSURAZIONE DEL CALCESTRUZZO COME PROCESSO A CATENA MARKOFFIANA,1982$fVIOLAE. 210 $aBologna$cI.S.D.C.$d1982 300 $aAtti dell'Istituto di Scienza delle Costruzioni dell'Università di Bologna. 610 0 $aAtti ed estratti di Università ed Istituti Universitari Italiani. 700 1$aViola,$bErasmo$f<1947- >$0333591 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990000608900403321 952 $a07 U/180$b$fDINSC 959 $aDINSC 996 $aSULL'EVOLUZIONE DEL DANNEGGIAMENTO PER MICROFESSURAZIONE DEL CALCESTRUZZO COME PROCESSO A CATENA MARKOFFIANA,1982$9317593 997 $aUNINA DB $aING01 LEADER 05776nam 2200781 a 450 001 9911020225903321 005 20200520144314.0 010 $a9781118587843 010 $a1118587847 010 $a9781118561829 010 $a1118561821 010 $a9781299187078 010 $a1299187072 010 $a9781118587904 010 $a1118587901 035 $a(CKB)2670000000327742 035 $a(EBL)1120893 035 $a(OCoLC)827207444 035 $a(SSID)ssj0000831564 035 $a(PQKBManifestationID)11437148 035 $a(PQKBTitleCode)TC0000831564 035 $a(PQKBWorkID)10873437 035 $a(PQKB)10372085 035 $a(OCoLC)828198474 035 $a(MiAaPQ)EBC1120893 035 $a(Perlego)1013113 035 $a(EXLCZ)992670000000327742 100 $a20120424d2012 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aIndustrial used of formal method $eformal verification /$fedited by Jean-Louis Boulanger 210 $aLondon $cISTE ;$aHoboken, N.J. $cWiley$dc2012 215 $a1 online resource (307 p.) 225 1 $aISTE 300 $aDescription based upon print version of record. 311 08$a9781848213630 311 08$a1848213638 320 $aIncludes bibliographical references and index. 327 $aCover; Title; Copyright; Table of Contents; Introduction; Chapter 1. SPARK - A Language and Tool-Set for High-Integrity Software Development; 1.1. Introduction; 1.2. An overview of SPARK; 1.2.1. What is SPARK?; 1.3. The rationale behind SPARK; 1.3.1. Flow analysis; 1.3.2. Code proof; 1.3.3. Correctness by construction; 1.4. Industrial applications of SPARK; 1.4.1. SHOLIS; 1.4.2. Lockheed-Martin C-130J mission computer; 1.4.3. MULTOS CA; 1.4.4. Tokeneer; 1.4.5. Aircraft monitoring software; 1.4.6. iFACTS; 1.4.7. SPARK Skein; 1.5. Conclusion; 1.6. Bibliography 327 $aChapter 2. Model-Based Testing Automatic Generationof Test Cases Using the Markov Chain Model2.1. Preliminaries on the test process; 2.1.1. Findings; 2.1.2. Test optimization; 2.1.3. The statistical usage test; 2.1.4. Generating test cases; 2.2. Modeling using Markov chains; 2.2.1. Origin; 2.2.2. Mathematical formalization; 2.2.3. Principles of generation; 2.2.4. Some indicators; 2.2.5. Calculating reliability; 2.3. The MaTeLo tool; 2.3.1. Engineering tests directed by models,model-based testing; 2.3.2. A chain of tools; 2.3.3. The usage model; 2.3.4. Configuration of test strategies 327 $a2.3.5. Generating test campaigns2.3.6. Analysis of the results and indicators; 2.4. Examples of industrial applications; 2.4.1. AUDI; 2.4.2. Magneti marelli; 2.4.3. Other industrial applications; 2.4.4. Industrialization of the tests; 2.5. Conclusion; 2.6. Bibliography; Chapter 3. Safety Analysis of the Embedded Systems with the AltaRica Approach; 3.1. Introduction; 3.2. Safety analysis of embedded systems; 3.3. AltaRica language and tools; 3.3.1. The AltaRica language; 3.3.2. Modeling the propagation of failures with AltaRica; 3.3.3. Tools associated with AltaRica 327 $a3.4. Examples of modeling and safety analysis3.4.1. Integrated modular avionics architecture; 3.4.2. System of electric power generation and distribution; 3.5. Comparison with other approaches; 3.5.1. Some precursors; 3.5.2. Tools for preexisting formal languages; 3.5.3. Languages for physical systems; 3.5.4. Injecting faults in nominal models; 3.6. Conclusion; 3.6.1. An approach to assess the safetyof systems tested in aeronautics; 3.6.2. Clarification of the system architectureand horizontal exploration of the failure propagation:impacts on the scope of analyses 327 $a3.6.3. Clarification of the nominal system characteristics:impacts on the generic definitions of the failure modes3.6.4. Compositional models of failure propagation:impacts on the overall safety process; 3.7. Special thanks; 3.8. Bibliography; Chapter 4. Polyspace®; 4.1. Overview; 4.2. Introduction to software quality and verification procedures; 4.3. Static analysis; 4.4. Dynamic tests; 4.5. Abstract interpretation; 4.6. Code verification; 4.7. Robustness verification or contextual verification; 4.7.1. Robustness verification; 4.7.2. Contextual verification 327 $a4.8. Examples of Polyspace® results 330 $a"At present the literature gives students and researchers of the very general books on the formal technics. The purpose of this book is to present in a single book, a return of experience on the used of the "formal technics" (such proof and model-checking) on industrial examples for the transportation domain.This book is based on the experience of people which are completely involved in the realization and the evaluation of safety critical system software based. The implication of the industrialists allows to raise the problems of confidentiality which could appear and so allow to supply new useful information (photos, plan of architecture, real example)"--$cProvided by publisher. 410 0$aISTE 606 $aSystems engineering$xData processing 606 $aComputer simulation 606 $aFormal methods (Computer science) 606 $aComputer software$xVerification 606 $aNondestructive testing 615 0$aSystems engineering$xData processing. 615 0$aComputer simulation. 615 0$aFormal methods (Computer science) 615 0$aComputer software$xVerification. 615 0$aNondestructive testing. 676 $a005.101 701 $aBoulanger$b Jean-Louis$0847395 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9911020225903321 996 $aIndustrial used of formal method$94417618 997 $aUNINA