Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Systèmes informatiques --- Télécommunications, Systèmes de --- Méthodes formelles (Informatique) --- Services Web

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Reactive systems are becoming more and more important for essentially all areas of technical and professional activities as well as for many areas of everyday life. The design of these systems is a great challenge and requires sound compromises between safety and time-to-market. To meet these needs, early design phases nowadays include verification of given specifications against system descriptions to find potential design errors as early as possible. This book is devoted to the foundation of the most popular formal methods for the specification and verification of reactive systems. In particular, the µ-calculus, omega-automata, and temporal logics are covered in full detail; their relationship and state-of-the-art verification procedures based on these formal approaches are presented. Furthermore, the advantages and disadvantages of the formalisms from particular points of view are analyzed. Most results are given with detailed proofs, so that the presentation is almost self-contained. This book is targeted to advanced students, lecturers and researchers in the area of formal methods.

Computer science --- Computer systems --- Formal methods (Computer science) --- Computer algorithms. --- Systèmes informatiques --- Méthodes formelles (Informatique) --- Algorithmes --- Verification. --- Vérification --- Computer algorithms --- Verification --- Formal methods (Computer science). --- Systèmes informatiques --- Méthodes formelles (Informatique) --- Vérification --- Computer systems - Verification

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

The aim of software engineering is the provision and investigation of methods for the development of software systems of high quality with correctness as a key issue. A system is called correct if it does what one wants, if it meets the requirements. To achieve and to guarantee correct systems, the need of formal methods with rigorous semantics and the possibility of verification is widely accepted. Algebraic specification is a software engineering approach of this perspective. When Liskov and Zilles, Guttag and the ADJ-group with Goguen, Thatch­ er, Wagner and Wright introduced the basic ideas of algebraic specification in the mid seventies in the U. S. A. and Canada, they initiated a very successful and still flourishing new area. In the late seventies, algebraic specification became a major research topic also in many European countries. Originally, the algebraic framework was intended for the mathematical foundation of ab­ stract data types and the formal development of first-order applicative pro­ grams. Meanwhile, the range of applications has been extended to the precise specification of complete software systems, the uniform definition of syntax and semantics of programming languages, and to the stepwise development of correct systems from the requirement definitions to the running programs. The activities in the last 25 years have led to an abundance of concepts, methods, approaches, theories, languages and tools, which are mathemati­ cally founded in universal algebra, category theory and logic.

Software engineering. --- Formal methods (Computer science) --- System design. --- Génie logiciel --- Méthodes formelles (Informatique) --- Systèmes, Conception de --- Software engineering --- System design --- Formal methods (Computer science). --- Génie logiciel --- Méthodes formelles (Informatique) --- Systèmes, Conception de --- Computer programming. --- Computer logic. --- Computer science—Mathematics. --- Programming Techniques. --- Software Engineering. --- Logics and Meanings of Programs. --- Mathematics of Computing. --- Computer science logic --- Logic, Symbolic and mathematical --- Computer software engineering --- Engineering --- Computers --- Electronic computer programming --- Electronic data processing --- Electronic digital computers --- Programming (Electronic computers) --- Coding theory --- Programming

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Formal methods (Computer science) --- Software engineering --- Méthodes formelles (Informatique) --- Génie logiciel --- Congresses --- Congrès --- Computer Science --- Engineering & Applied Sciences --- Méthodes formelles (Informatique) --- Génie logiciel --- Congrès --- Computer science. --- Software engineering. --- Programming languages (Electronic computers). --- Computer logic. --- Computer Science. --- Software Engineering/Programming and Operating Systems. --- Software Engineering. --- Programming Languages, Compilers, Interpreters. --- Logics and Meanings of Programs. --- Logic design. --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Informatics --- Science --- Computer software engineering --- Engineering --- Computer science logic --- Logic, Symbolic and mathematical --- Computer languages --- Computer program languages --- Computer programming languages --- Machine language --- Electronic data processing --- Languages, Artificial --- Formal methods (Computer science) - Congresses --- Software engineering - Congresses

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Traditionally, models and methods for the analysis of the functional correctness of reactive systems, and those for the analysis of their performance (and - pendability) aspects, have been studied by di?erent research communities. This has resulted in the development of successful, but distinct and largely unrelated modeling and analysis techniques for both domains. In many modern systems, however, the di?erence between their functional features and their performance properties has become blurred, as relevant functionalities become inextricably linked to performance aspects, e.g. isochronous data transfer for live video tra- mission. During the last decade, this trend has motivated an increased interest in c- bining insights and results from the ?eld of formal methods – traditionally - cused on functionality – with techniques for performance modeling and analysis. Prominent examples of this cross-fertilization are extensions of process algebra and Petri nets that allow for the automatic generation of performance models, the use of formal proof techniques to assess the correctness of randomized - gorithms, and extensions of model checking techniques to analyze performance requirements automatically. We believe that these developments markthe - ginning of a new paradigm for the modeling and analysis of systems in which qualitative and quantitative aspects are studied from an integrated perspective. We are convinced that the further worktowards the realization of this goal will be a growing source of inspiration and progress for both communities.

Formal methods (Computer science) --- Computer Science --- Engineering & Applied Sciences --- Méthodes formelles (Informatique) --- Congresses --- Congrès --- Méthodes formelles (Informatique) --- Congrès --- Computer science. --- Computer communication systems. --- Computer system failures. --- Software engineering. --- Computer logic. --- Computer engineering. --- Computer Science. --- Software Engineering/Programming and Operating Systems. --- Computer Engineering. --- Logics and Meanings of Programs. --- Software Engineering. --- System Performance and Evaluation. --- Computer Communication Networks. --- Logic design. --- Computer system performance. --- Computer software engineering --- Engineering --- Design, Logic --- Design of logic systems --- Digital electronics --- Electronic circuit design --- Logic circuits --- Machine theory --- Switching theory --- Communication systems, Computer --- Computer communication systems --- Data networks, Computer --- ECNs (Electronic communication networks) --- Electronic communication networks --- Networks, Computer --- Teleprocessing networks --- Data transmission systems --- Digital communications --- Electronic systems --- Information networks --- Telecommunication --- Cyberinfrastructure --- Electronic data processing --- Network computers --- Computer failures --- Computer malfunctions --- Computer systems --- Failure of computer systems --- System failures (Engineering) --- Fault-tolerant computing --- Computer science logic --- Logic, Symbolic and mathematical --- Computers --- Distributed processing --- Failures --- Design and construction --- Formal methods (Computer science) - Congresses