- Table View
- List View
Formal Methods for Distributed System Development: FORTE / PSTV 2000 IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XIII) and Protocol Specification, Testing and Verification (PSTV XX) October 10–13, 2000, Pisa, Italy (IFIP Advances in Information and Communication Technology #55)
by Tommaso Bolognesi Diego Latellath The 20 anniversary of the IFIP WG6. 1 Joint International Conference on Fonna! Methods for Distributed Systems and Communication Protocols (FORTE XIII / PSTV XX) was celebrated by the year 2000 edition of the Conference, which was held for the first time in Italy, at Pisa, October 10-13, 2000. In devising the subtitle for this special edition --'Fonna! Methods Implementation Under Test' --we wanted to convey two main concepts that, in our opinion, are reflected in the contents of this book. First, the early, pioneering phases in the development of Formal Methods (FM's), with their conflicts between evangelistic and agnostic attitudes, with their over optimistic applications to toy examples and over-skeptical views about scalability to industrial cases, with their misconceptions and myths . . . , all this is essentially over. Many FM's have successfully reached their maturity, having been 'implemented' into concrete development practice: a number of papers in this book report about successful experiences in specifYing and verifYing real distributed systems and protocols. Second, one of the several myths about FM's - the fact that their adoption would eventually eliminate the need for testing - is still quite far from becoming a reality, and, again, this book indicates that testing theory and applications are still remarkably healthy. A total of 63 papers have been submitted to FORTEIPSTV 2000, out of which the Programme Committee has selected 22 for presentation at the Conference and inclusion in the Proceedings.
Formal Methods for Mining Structured Objects (Studies in Computational Intelligence #475)
by Gemma C GarrigaIn the field of knowledge discovery, graphs of concepts are an expressive and versatile modeling technique providing ways to reason about information implicit in a set of data. Interesting examples of this can be found under the mathematical theory of formal concept analysis, dedicated to the construction of a lattice of concepts by defining a Galois connection on a binary relationship. This book present such graph of concepts under the more complex case of data that comes in a set of structured objects; e.g. a set of sequences, trees or graphs. Nodes of this graph will represent patterns in the data and edges will correspond to relationships of specificity. From this combinatorial object results are derived such as a full characterization of logical implications and closed partial orders. The results presented in this book are coupled with examples and empirical experiments that illustrate the derived theoretical contributions.
Formal Methods for Open Object-based Distributed Systems: Volume 2 (IFIP Advances in Information and Communication Technology)
by Howard Bowman John DerrickThis book presents the leading edge in several related fields, specifically object orientated programming, open distributed systems and formal methods for object oriented systems. With increased support within industry regarding these areas, this book captures the most up-to-date information on the subject. Many topics are discussed, including the following important areas: object oriented design and programming; formal specification of distributed systems; open distributed platforms; types, interfaces and behaviour; formalisation of object oriented methods.
Formal Methods for Open Object-based Distributed Systems: Volume 1 (IFIP Advances in Information and Communication Technology)
by Elie Najm Jean-Bernard StefaniObject-based Distributed Computing is being established as the most pertinent basis for the support of large, heterogeneous computing and telecommunications systems. The advent of Open Object-based Distributed Systems (OODS) brings new challenges and opportunities for the use and development of formal methods. Formal Methods for Open Object-based Distributed Systems presents the latest research in several related fields, and the exchange of ideas and experiences in a number of topics including: formal models for object-based distributed computing; semantics of object-based distributed systems and programming languages; formal techniques in object-based and object oriented specification, analysis and design; refinement and transformation of specifications; multiple viewpoint modeling and consistency between different models; formal techniques in distributed systems verification and testing; types, service types and subtyping; specification, verification and testing of quality of service constraints and formal methods and the object life cycle. It contains the selected proceedings of the International Workshop on Formal Methods for Open Object-based Distributed Systems, sponsored by the International Federation for Information Processing, and based in Paris, France, in March 1996.
Formal Methods for Protocol Engineering and Distributed Systems: Forte XII / PSTV XIX’99 (IFIP Advances in Information and Communication Technology #28)
by Jianping Jianping Wu Samuel T. Chanson Quiang Quiang GaoFormal Methods for Protocol Engineering and Distributed Systems addresses formal description techniques (FDTs) applicable to distributed systems and communication protocols. It aims to present the state of the art in theory, application, tools an industrialization of FDTs. Among the important features presented are: FDT-based system and protocol engineering; FDT application to distributed systems; Protocol engineeering; Practical experience and case studies. Formal Methods for Protocol Engineering and Distributed Systems contains the proceedings of the Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing, and Verification, which was sponsored by the International Federation for Information Processing (IFIP) and was held in Beijing, China, in October 1999. This volume is suitable as a secondary text for a graduate level course on Distributed Systems or Communications, and as a reference for researchers and industry practitioners.
Formal Methods for Safety and Security: Case Studies for Aerospace Applications
by Manju Nanda Yogananda JeppuThis volume is the outcome of deliberations on formal methods in aerospace. The book specially delves into the use of formal methods for verification, validation, and optimization of software in safety critical and time critical applications, such as those in aerospace engineering. The chapters in this book are authored by leading corporate and government R&D scientists. The contents of this book will be useful to researchers and professionals alike.
Formal Methods for Software Engineering: Languages, Methods, Application Domains (Texts in Theoretical Computer Science. An EATCS Series)
by Antonio Cerone Siraj Ahmed Shaikh Markus Roggenbach Gerardo Schneider Bernd-Holger SchlingloffSoftware programs are formal entities with precise meanings independent of their programmers, so the transition from ideas to programs necessarily involves a formalisation at some point. The first part of this graduate-level introduction to formal methods develops an understanding of what constitutes formal methods and what their place is in Software Engineering. It also introduces logics as languages to describe reasoning and the process algebra CSP as a language to represent behaviours. The second part offers specification and testing methods for formal development of software, based on the modelling languages CASL and UML. The third part takes the reader into the application domains of normative documents, human machine interfaces, and security. Use of notations and formalisms is uniform throughout the book. Topics and features: Explains foundations, and introduces specification, verification, and testing methods Explores various application domains Presents realistic and practical examples, illustrating concepts Brings together contributions from highly experienced educators and researchers Offers modelling and analysis methods for formal development of software Suitable for graduate and undergraduate courses in software engineering, this uniquely practical textbook will also be of value to students in informatics, as well as to scientists and practical engineers, who want to learn about or work more effectively with formal theories and methods. Markus Roggenbach is a Professor in the Dept. of Computer Science of Swansea University. Antonio Cerone is an Associate Professor in the Dept. of Computer Science of Nazarbayev University, Nur-Sultan. Bernd-Holger Schlingloff is a Professor in the Institut für Informatik of Humboldt-Universität zu Berlin. Gerardo Schneider is a Professor in the Dept. of Computer Science and Engineering of University of Gothenburg. Siraj Ahmed Shaikh is a Professor in the Institute for Future Transport and Cities of Coventry University.
Formal Methods in Architecture: Proceedings of the 5th International Symposium on Formal Methods in Architecture (5FMA), Lisbon 2020 (Advances in Science, Technology & Innovation)
by Sara Eloy David Leite Viana Franklim Morais Jorge Vieira VazThis edited book gathers research studies presented at the 5th International Symposium on Formal Methods in Architecture (5FMA), Lisbon 2020. Studies focus on the use of methodologies, especially those that have witnessed recent developments, that stem from the mathematical and computer sciences and are developed in a collaborative way with architecture and related fields. This book constitutes a contribution to the debate and to the introduction of new methodologies and tools in the mentioned fields that derive from the application of formal methods in the creation of new explicit languages for problem-solving in architecture and urbanism. It adds valuable insight into the development of new practices solving identified societal problems and promoting the digital transformation of institutions in the mentioned fields. The primary audience of this book will be from the fields of architecture, urban planning, civil engineering, AEC, landscape design, computer sciences and mathematics, both academicians and professionals.
Formal Methods in Architecture: Proceedings of the 6th International Symposium on Formal Methods in Architecture (6FMA), A Coruña 2022 (Digital Innovations in Architecture, Engineering and Construction)
by Plácido Lizancos Mora David Leite Viana Franklim Morais Jorge Vieira VazThis book comprises the select proceedings of the 6th International Symposium on Formal Methods in Architecture (6FMA), A Coruña 2022. The contents focus on the use of methodologies, especially those that have witnessed recent developments stemming from mathematical and computer sciences and are developed in a collaborative way with architecture and related fields. This book constitutes a contribution to the debate and to the introduction of new methodologies and tools in the mentioned fields that derive from the application of formal methods in the creation of new explicit languages for problem-solving in architecture and urbanism. Some of the themes in the book are CAD and BIM, mixed realities, photogrammetry and 3D scan, architectural design automation, urban and building performance analysis, SCAVA-space configuration, accessibility and visibility analysis. This book proves a valuable resource for those in academia and industry.
Formal Methods in Computer-Aided Design: 4th International Conference, FMCAD 2002, Portland, OR, USA, November 6-8, 2002, Proceedings (Lecture Notes in Computer Science #2517)
by Mark D. Aagaard John W. O'LearyThis volume contains the proceedings of the Fourth Biennial Conference on F- mal Methods in Computer-Aided Design (FMCAD). The conference is devoted to the use of mathematical methods for the analysis of digital hardware c- cuits and systems. The workreported in this bookdescribes the use of formal mathematics and associated tools to design and verify digital hardware systems. Functional veri?cation has become one of the principal costs in a modern computer design e?ort. FMCAD provides a venue for academic and industrial researchers and practitioners to share their ideas and experiences of using - screte mathematical modeling and veri?cation. Over the past 20 years, this area has grown from just a few academic researchers to a vibrant worldwide com- nity of people from both academia and industry. This volume includes 23 papers selected from the 47 submitted papers, each of which was reviewed by at least three program committee members. The history of FMCAD dates backto 1984, when the earliest meetings on this topic occurred as part of IFIP WG10.2.
Formal Methods in Computer-Aided Design: Second International Conference, FMCAD '98, Palo Alto, CA, USA, November 4-6, 1998, Proceedings (Lecture Notes in Computer Science #1522)
by Ganesh Gopalakrishnan Phillip WindleyFormal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1-3, 2000 Proceedings (Lecture Notes in Computer Science #1954)
by Warren A. Jr. Hunt Steven D. JohnsonThe biannual Formal Methods in Computer Aided Design conference (FMCAD 2000)is the third in a series of conferences under that title devoted to the use of discrete mathematical methods for the analysis of computer hardware and so- ware. The work reported in this book describes the use of modeling languages and their associated automated analysis tools to specify and verify computing systems. Functional veric ation has become one of the principal costs in a modern computer design e ort. In addition,verica tion of circuit models, timing,power, etc., requires even more eo rt. FMCAD provides a venue for academic and - dustrial researchers and practitioners to share their ideas and experiences of using discrete mathematical modeling and veric ation. It is noted with interest by the conference chairmen how this area has grown from just a few people 15 years ago to a vibrant area of research, development, and deployment. It is clear that these methods are helping reduce the cost of designing computing systems. As an example of this potential cost reduction, we have invited David Russino of Advanced Micro Devices, Inc. to describe his veric ation of ?oating-point - gorithms being used in AMD microprocessors. The program includes 30 regular presentations selected from 63 submitted papers.
Formal Methods in Manufacturing (Industrial Information Technology)
by Javier Campos Carla Seatzu Xiaolan XieIllustrated with real-life manufacturing examples, Formal Methods in Manufacturing provides state-of-the-art solutions to common problems in manufacturing systems. Assuming some knowledge of discrete event systems theory, the book first delivers a detailed introduction to the most important formalisms used for the modeling, analysis, and control of manufacturing systems (including Petri nets, automata, and max-plus algebra), explaining the advantages of each formal method. It then employs the different formalisms to solve specific problems taken from today’s industrial world, such as modeling and simulation, supervisory control (including deadlock prevention) in a distributed and/or decentralized environment, performance evaluation (including scheduling and optimization), fault diagnosis and diagnosability analysis, and reconfiguration. Containing chapters written by leading experts in their respective fields, Formal Methods in Manufacturing helps researchers and application engineers handle fundamental principles and deal with typical quality goals in the design and operation of manufacturing systems.
Formal Methods in Manufacturing (Industrial Information Technology)
by Javier Campos Carla Seatzu Xiaolan XieIllustrated with real-life manufacturing examples, Formal Methods in Manufacturing provides state-of-the-art solutions to common problems in manufacturing systems. Assuming some knowledge of discrete event systems theory, the book first delivers a detailed introduction to the most important formalisms used for the modeling, analysis, and control of manufacturing systems (including Petri nets, automata, and max-plus algebra), explaining the advantages of each formal method. It then employs the different formalisms to solve specific problems taken from today’s industrial world, such as modeling and simulation, supervisory control (including deadlock prevention) in a distributed and/or decentralized environment, performance evaluation (including scheduling and optimization), fault diagnosis and diagnosability analysis, and reconfiguration. Containing chapters written by leading experts in their respective fields, Formal Methods in Manufacturing helps researchers and application engineers handle fundamental principles and deal with typical quality goals in the design and operation of manufacturing systems.
Formal Modeling and Verification of Cyber-Physical Systems: 1st International Summer School on Methods and Tools for the Design of Digital Systems, Bremen, Germany, September 2015
by Rolf Drechsler Ulrich KühneThis book presents the lecture notes of the 1st Summer School on Methods and Tools for the Design of Digital Systems, 2015, held in Bremen, Germany. The topic of the summer school was devoted to modeling and verification of cyber-physical systems. This covers several aspects of the field, including hybrid systems and model checking, as well as applications in robotics and aerospace systems.The main chapters have been written by leading scientists, who present their field of research, each providing references to introductory material as well as latest scientific advances and future research directions. This is complemented by short papers submitted by the participating PhD students.
Formal Semantics and Proof Techniques for Optimizing VHDL Models
by Kothanda Umamageswaran Sheetanshu L. Pandey Philip A. WilseyWritten expressly for hardware designers, this book presents a formal model of VHDL clearly specifying both the static and dynamic semantics of VHDL. It provides a mathematical framework for representing VHDL constructs and shows how those constructs can be formally manipulated to reason about VHDL.
Formal Semantics for VHDL (The Springer International Series in Engineering and Computer Science #307)
by Carlos Delgado Kloos P. BreuerIt is recognized that formal design and verification methods are an important requirement for the attainment of high quality system designs. The field has evolved enormously during the last few years, resulting in the fact that formal design and verification methods are nowadays supported by several tools, both commercial and academic. If different tools and users are to generate and read the same language then it is necessary that the same semantics is assigned by them to all constructs and elements of the language. The current IEEE standard VHDL language reference manual (LRM) tries to define VHDL as well as possible in a descriptive way, explaining the semantics in English. But rigor and clarity are very hard to maintain in a semantics defined in this way, and that has already given rise to many misconceptions and contradictory interpretations. Formal Semantics for VHDL is the first book that puts forward a cohesive set of semantics for the VHDL language. The chapters describe several semantics each based on a different underlying formalism: two of them use Petri nets as target language, and two of them higher order logic. Two use functional concepts, and finally another uses the concept of evolving algebras. Formal Semantics for VHDL is essential reading for researchers in formal methods and can be used as a text for an advanced course on the subject.
Formal Specification Level: Concepts, Methods, and Algorithms
by Mathias Soeken Rolf DrechslerThis book introduces a new level of abstraction that closes the gap between the textual specification of embedded systems and the executable model at the Electronic System Level (ESL). Readers will be enabled to operate at this new, Formal Specification Level (FSL), using models which not only allow significant verification tasks in this early stage of the design flow, but also can be extracted semi-automatically from the textual specification in an interactive manner. The authors explain how to use these verification tasks to check conceptual properties, e.g. whether requirements are in conflict, as well as dynamic behavior, in terms of execution traces.
Formal System Verification: State-of the-Art and Future Trends
by Rolf DrechslerThis book provides readers with a comprehensive introduction to the formal verification of hardware and software. World-leading experts from the domain of formal proof techniques show the latest developments starting from electronic system level (ESL) descriptions down to the register transfer level (RTL). The authors demonstrate at different abstraction layers how formal methods can help to ensure functional correctness. Coverage includes the latest academic research results, as well as descriptions of industrial tools and case studies.
Formal Techniques for Networked and Distributed Systems: FORTE 2001 (IFIP Advances in Information and Communication Technology #69)
by Myungchul Myungchul Kim Byoungmoon Byoungmoon Chin Sungwon Sungwon Kang Danhyung Danhyung LeeFORTE 2001, formerly FORTE/PSTV conference, is a combined conference of FORTE (Formal Description Techniques for Distributed Systems and Communication Protocols) and PSTV (Protocol Specification, Testing and Verification) conferences. This year the conference has a new name FORTE (Formal Techniques for Networked and Distributed Systems). The previous FORTE began in 1989 and the PSTV conference in 1981. Therefore the new FORTE conference actually has a long history of 21 years. The purpose of this conference is to introduce theories and formal techniques applicable to various engineering stages of networked and distributed systems and to share applications and experiences of them. This FORTE 2001 conference proceedings contains 24 refereed papers and 4 invited papers on the subjects. We regret that many good papers submitted could not be published in this volume due to the lack of space. FORTE 2001 was organized under the auspices of IFIP WG 6.1 by Information and Communications University of Korea. It was financially supported by Ministry of Information and Communication of Korea. We would like to thank every author who submitted a paper to FORTE 2001 and thank the reviewers who generously spent their time on reviewing. Special thanks are due to the reviewers who kindly conducted additional reviews for rigorous review process within a very short time frame. We would like to thank Prof. Guy Leduc, the chairman of IFIP WG 6.1, who made valuable suggestions and shared his experiences for conference organization.
Formal Techniques in Real-Time and Fault-Tolerant Systems (The Springer International Series in Engineering and Computer Science #221)
by Jan VytopilFormal Techniques in Real-Time and Fault-Tolerant Systems focuses on the state of the art in formal specification, development and verification of fault-tolerant computing systems. The term `fault-tolerance' refers to a system having properties which enable it to deliver its specified function despite (certain) faults of its subsystem. Fault-tolerance is achieved by adding extra hardware and/or software which corrects the effects of faults. In this sense, a system can be called fault-tolerant if it can be proved that the resulting (extended) system under some model of reliability meets the reliability requirements. The main theme of Formal Techniques in Real-Time and Fault-Tolerant Systems can be formulated as follows: how do the specification, development and verification of conventional and fault-tolerant systems differ? How do the notations, methodology and tools used in design and development of fault-tolerant and conventional systems differ? Formal Techniques in Real-Time and Fault-Tolerant Systems is divided into two parts. The chapters in Part One set the stage for what follows by defining the basic notions and practices of the field of design and specification of fault-tolerant systems. The chapters in Part Two represent the `how-to' section, containing examples of the use of formal methods in specification and development of fault-tolerant systems. The book serves as an excellent reference for researchers in both academia and industry, and may be used as a text for advanced courses on the subject.
Formal Verification of Circuits
by Rolf DrechslerFormal verification has become one of the most important steps in circuit design. Since circuits can contain several million transistors, verification of such large designs becomes more and more difficult. Pure simulation cannot guarantee the correct behavior and exhaustive simulation is often impossible. However, many designs, like ALUs, have very regular structures that can be easily described at a higher level of abstraction. For example, describing (and verifying) an integer multiplier at the bit-level is very difficult, while the verification becomes easy when the outputs are grouped to build a bit-string. Recently, several approaches for formal circuit verification have been proposed that make use of these regularities. These approaches are based on Word-Level Decision Diagrams (WLDDs) which are graph-based representations of functions (similar to BDDs) that allow for the representation of functions with a Boolean range and an integer domain. Formal Verification of Circuits is devoted to the discussion of recent developments in the field of decision diagram-based formal verification. Firstly, different types of decision diagrams (including WLDDs) are introduced and theoretical properties are discussed that give further insight into the data structure. Secondly, implementation and minimization concepts are presented. Applications to arithmetic circuit verification and verification of designs specified by hardware description languages are described to show how WLDDs work in practice. Formal Verification of Circuits is intended for CAD developers and researchers as well as designers using modern verification tools. It will help people working with formal verification (in industry or academia) to keep informed about recent developments in this area.
Formal Verification of Floating-Point Hardware Design: A Mathematical Approach
by David M. RussinoffThis is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods. Formal Verification of Floating-Point Hardware Design, Second Edition advances a verification methodology based on a unified theory of register-transfer logic and floating-point arithmetic that has been developed and applied to the formal verification of commercial floating-point units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. The theory is extended to the analysis of several algorithms and optimization techniques that are commonly used in commercial implementations of elementary arithmetic operations. As a basis for the formal verification of such implementations, high-level specifications of the basic arithmetic instructions of several major industry-standard floating-point architectures are presented, including all details pertaining to the handling of exceptional conditions. The methodology is illustrated in the comprehensive verification of a variety of state-of-the-art commercial floating-point designs developed by Arm Holdings. This revised edition reflects the evolving microarchitectures and increasing sophistication of Arm processors, and the variation in the design goals of execution speed, hardware area requirements, and power consumption. Many new results have been added to Parts I—III (Register-Transfer Logic, Floating-Point Arithmetic, and Implementation of Elementary Operations), extending the theory and describing new techniques. These were derived as required in the verification of the new RTL designs described in Part V.
Formal Verification of Floating-Point Hardware Design: A Mathematical Approach
by David M. Russinoff J Strother MooreThis is the first book to focus on the problem of ensuring the correctness of floating-point hardware designs through mathematical methods. Formal Verification of Floating-Point Hardware Design advances a verification methodology based on a unified theory of register-transfer logic and floating-point arithmetic that has been developed and applied to the formal verification of commercial floating-point units over the course of more than two decades, during which the author was employed by several major microprocessor design companies. The book consists of five parts, the first two of which present a rigorous exposition of the general theory based on the first principles of arithmetic. Part I covers bit vectors and the bit manipulation primitives, integer and fixed-point encodings, and bit-wise logical operations. Part II addresses the properties of floating-point numbers, the formats in which they are encoded as bit vectors, and the various modes of floating-point rounding. In Part III, the theory is extended to the analysis of several algorithms and optimization techniques that are commonly used in commercial implementations of elementary arithmetic operations. As a basis for the formal verification of such implementations, Part IV contains high-level specifications of correctness of the basic arithmetic instructions of several major industry-standard floating-point architectures, including all details pertaining to the handling of exceptional conditions. Part V illustrates the methodology, applying the preceding theory to the comprehensive verification of a state-of-the-art commercial floating-point unit. All of these results have been formalized in the logic of the ACL2 theorem prover and mechanically checked to ensure their correctness. They are presented here, however, in simple conventional mathematical notation. The book presupposes no familiarity with ACL2, logic design, or any mathematics beyond basic high school algebra. It will be of interest to verification engineers as well as arithmetic circuit designers who appreciate the value of a rigorous approach to their art, and is suitable as a graduate text in computer arithmetic.
Formal Verification of Simulink/Stateflow Diagrams: A Deductive Approach
by Naijun Zhan Shuling Wang Hengjun ZhaoThis book presents a state-of-the-art technique for formal verification of continuous-time Simulink/Stateflow diagrams, featuring an expressive hybrid system modelling language, a powerful specification logic and deduction-based verification approach, and some impressive, realistic case studies. Readers will learn the HCSP/HHL-based deductive method and the use of corresponding tools for formal verification of Simulink/Stateflow diagrams. They will also gain some basic ideas about fundamental elements of formal methods such as formal syntax and semantics, and especially the common techniques applied in formal modelling and verification of hybrid systems. By investigating the successful case studies, readers will realize how to apply the pure theory and techniques to real applications, and hopefully will be inspired to start to use the proposed approach, or even develop their own formal methods in their future work.