Аннотация к книге "Specification and Seamless Verification of Embedded Real-Time Systems. FOCUS on Isabelle"
The purpose of this thesis is to create a coupling of the formal specification framework Focus in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of systems that are especially safety critical - embedded real-time systems. The specification and verification/validation methodologies are treated as a single, joined, methodology with the main focus on the specification part. The key...
The purpose of this thesis is to create a coupling of the formal specification framework Focus in the generic theorem prover Isabelle/HOL, a logical framework based on Higher-Order Logic. The main focus of this work is on specification and verification of systems that are especially safety critical - embedded real-time systems. The specification and verification/validation methodologies are treated as a single, joined, methodology with the main focus on the specification part. The key contributions of the thesis are + Embedding of that part of the framework Focus, which is appropriate for the specification of real-time systems, into Isabelle/HOL. "Focus on Isabelle" enables to validate and verify system specifications in a methodological way. + Syntax extensions for Focus for the argumentation over time intervals: a special kind of tables, timed state transition diagrams, and a number of new operators. The deep embedding into Isabelle/HOL includes all these extensions. + Schemata for automatic correctness proofs in Isabelle/HOL of the syntactic interfaces for specified system components.
Данное издание не является оригинальным. Книга печатается по технологии принт-он-деманд после получения заказа.
С наступлением весны гномы, живущие на берегу ручья Причудь, решают отправиться в путешествие, чтобы найти своего друга, ушедшего в верховья ручья на поиски его истока. Впереди их ждут неизведанные земли, захватывающие приключения и удивительные открытия. Гномы пройдут опасные водовороты и страшный Вороний лес, сразятся с великаном Громобоем, окажутся на необитаемом острове и обретут множество новых...
Каким бы опытом программирования на JavaScript вы ни обладали, скорее всего, вы не понимаете язык в полной мере. Это лаконичное, но при этом глубоко продуманное руководство познакомит вас с областями видимости, замыканиями, ключевым словом this и объектами – концепциями, которые необходимо знать для более эффективного и производительного программирования на JS. Вы узнаете, как и почему они работают, и как...
Стандартная библиотека Python содержит сотни модулей, позволяющих взаимодействовать с операционной системой, интерпретатором и Интернетом. Все они тщательно протестированы и готовы к немедленному использованию для разработки приложений. В этой книге Даг Хеллман, эксперт по языку Python, описывает все основные разделы библиотеки Python 3.x, сопровождая изложение материала компактными примерами исходного кода и...
Оставить комментарий