دانلود کتاب Formal Methods for Industrial Critical Systems: A Survey of Applications

Today, formal methods are widely recognized as an essential step in the design process of industrial safety-critical systems. In its more general definition, the term formal methods encompasses all notations having a precise mathematical semantics, together with their associated analysis methods, that allow description and reasoning about the behavior of a system in a formal manner. Growing out of more than a decade of award-winning collaborative work within the European Research Consortium for Informatics and Mathematics, Formal Methods for Industrial Critical Systems: A Survey of Applications presents a number of mainstream formal methods currently used for designing industrial critical systems, with a focus on model checking. The purpose of the book is threefold: to reduce the effort required to learn formal methods, which has been a major drawback for their industrial dissemination; to help designers to adopt the formal methods which are most appropriate for their systems; and to offer a panel of state-of-the-art techniques and tools for analyzing critical systems.Content: Chapter 1 Formal Methods: Applying {Logics in, Theoretical} Computer Science (pages 1–14): Diego LatellaChapter 2 A Synchronous Language at Work: The Story of Lustre (pages 15–31): Nicolas HalbwachsChapter 3 Requirements of an Integrated Formal Method for Intelligent Swarms (pages 33–59): Mike Hinchey, James L. Rash, Christopher A. Rouff, Walt F. Truszkowski and Amy K. C. S. VanderbiltChapter 4 Some Trends in Formal Methods Applications to Railway Signaling (pages 61–84): Alessandro Fantechi, Wan Fokkink and Angelo MorzentiChapter 5 Symbolic Model Checking for Avionics (pages 85–112): Radu I. Siminiceanu and Gianfranco CiardoChapter 6 Applying Formal Methods to Telecommunication Services with Active Networks (pages 113–132): Maria del Mar Gallardo, Jesus Martinez and Pedro MerinoChapter 7 Practical Applications of Probabilistic Model Checking to Communication Protocols (pages 133–150): Marie Duflot, Marta Kwiatkowska, Gethin Norman, David Parker, Sylvain Peyronnet, Claudine Picaronny and Jeremy SprostonChapter 8 Design for Verifiability: The OCS Case Study (pages 151–177): Johannes Neubauer, Tiziana Margaria and Bernhard SteffenChapter 9 An Application of Stochastic Model Checking in the Industry: User?Centered Modeling and Analysis of Collaboration in Thinkteam® (pages 179–203): Maurice H. ter Beek, Stefania Gnesi, Diego Latella, Mieke Massink, Maurizio Sebastianis and Gianluca TrentanniChapter 10 The Testing and Test Control Notation TTCN?3 and its Use (pages 205–233): Ina Schieferdecker and Alain?Georges Vouffo?FeudjioChapter 11 Practical Aspects of Active Automata Learning (pages 235–267): Falk Howar, Maik Merten, Bernhard Steffen and Tiziana Margaria