Название «временная логика» может звучать сложно и устрашающе, но хотя временные логики описывают потенциально сложные сценарии, они часто основаны на нескольких простых и фундаментальных концепциях, освещенных в этой книге. «Введение в практические формальные методы с использованием временной логики» представляет введение в формальные методы, основанные на временной логике, для разработки и тестирования сложных вычислительных систем. Эти методы поддерживаются многими хорошо разработанными инструментами, методиками и результатами, которые могут применяться к широкому кругу систем. Фишер начинает с полного введения в предмет, охватывая основы временной логики и используя различные примеры, упражнения и ссылки на более продвинутые работы, чтобы прояснить и проиллюстрировать обсуждаемые темы. Затем он описывает, как эту логику можно использовать для спецификации различных вычислительных систем, рассматривая вопросы связывания спецификаций, параллелизма, связи и способности к композиции. Далее он анализирует методы временной спецификации, такие как дедуктивная верификация, алгоритмическая верификация и прямое выполнение, для разработки и проверки вычислительных систем. В заключительной главе описываются возможные проблемы, которые могут возникнуть в различных инженерных приложениях в области робототехники, сигнализации на железных дорогах, проектирования аппаратного обеспечения, повсеместных вычислений, интеллектуальных агентов и информационной безопасности, и объясняется, как временная логика может повысить их точность и надежность. Книга моделирует временные понятия и использует их для анализа вычислительных систем, предлагает широкий подход к временной логике во многих формальных методах, включая спецификацию, верификацию и реализацию, а также знакомит с бесплатными инструментами, основанными на временных логиках, и показывает, как их можно применять на практике.
The title "An Introduction to Practical Fomal Methods Using Temporail Logic" sounds complicated but it's really not. This book is an introduction to practical formal methods based on the subject of "temporail logic," or how to develop, test, and specify complex computational systems using temporal logics. Many tools and techniques are used for these systems, such as verification methods, algorithmic methods, and direct-execution methods.
Michael Fisher starts with providing a thorough introduction into the subject in order to clarify major concepts related to temporail logic. Through a variety of samples, questions, and additional references he helps illustrate the concepts that are discussed. Later, Fisher explains how to use this logic for a number of computational specifications, addressing topics such as interfacing details, parallel processing, information processing, component integration. He also discusses methods used in specification of systems like deduction, programming checks, and in-process enforcement to enhance the development and checking of computational systems. Finally, he highlights several valuable examples from autonomous robots, railway signaling, hardware development, mobile computing devices, computerized assistants, and data codification in business and government, illustrating how better standards could be achieved by utilizing temporail logics methods for analysis and specification.
Электронная Книга «An Introduction to Practical Formal Methods Using Temporal Logic» написана автором Michael Fisher в году.
Минимальный возраст читателя: 0
Язык: Английский
ISBN: 9781119991489
Описание книги от Michael Fisher
The name «temporal logic» may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts – highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems. Fisher begins with a full introduction to the subject, covering the basics of temporal logic and using a variety of examples, exercises and pointers to more advanced work to help clarify and illustrate the topics discussed. He goes on to describe how this logic can be used to specify a variety of computational systems, looking at issues of linking specifications, concurrency, communication and composition ability. He then analyses temporal specification techniques such as deductive verification, algorithmic verification, and direct execution to develop and verify computational systems. The final chapter on case studies analyses the potential problems that can occur in a range of engineering applications in the areas of robotics, railway signalling, hardware design, ubiquitous computing, intelligent agents, and information security, and explains how temporal logic can improve their accuracy and reliability. Models temporal notions and uses them to analyze computational systems Provides a broad approach to temporal logic across many formal methods – including specification, verification and implementation Introduces and explains freely available tools based on temporal logics and shows how these can be applied Presents exercises and pointers to further study in each chapter, as well as an accompanying website providing links to additional systems based upon temporal logic as well as additional material related to the book.
