- Table View
- List View
Formal Techniques for Safety-Critical Systems: 7th International Workshop, FTSCS 2019, Shenzhen, China, November 9, 2019, Revised Selected Papers (Communications in Computer and Information Science #1165)
by Osman Hasan Frédéric MalletThis book constitutes the refereed proceedings of the 7th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2019, held in Shenzhen, China, in November 2019.The 6 revised full papers presented were carefully reviewed and selected from 17 submissions. Additionally, the volume presents 1 invited paper, 1 tool paper, and 1 work in progrerss. The papers are focused on the topics of the use of formal methods for analyzing safety-critical systems; methods, techniques and tools to support automated analysis, certication, debugging, etc., of complex safety/QoS-critical systems; analysis methods that address the limitations of formal methods in industry (usability, scalability, etc.); formal analysis support for modeling languages used in industry; code generation from validated models.
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 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 Simulink/Stateflow Diagrams
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.
Formal Verification of Structurally Complex Multipliers
by Rolf Drechsler Daniel Große Alireza MahzoonThis book addresses the challenging tasks of verifying and debugging structurally complex multipliers. In the area of verification, the authors first investigate the challenges of Symbolic Computer Algebra (SCA)-based verification, when it comes to proving the correctness of multipliers. They then describe three techniques to improve and extend SCA: vanishing monomials removal, reverse engineering, and dynamic backward rewriting. This enables readers to verify a wide variety of multipliers, including highly complex and optimized industrial benchmarks. The authors also describe a complete debugging flow, including bug localization and fixing, to find the location of bugs in structurally complex multipliers and make corrections.
Formal and Practical Techniques for the Complex System Design Process using Virtual Prototypes: Better Early than Never
by Rolf Drechsler Pascal PieperThis book deals with formal and practical approaches for early fast modeling and verification of complex digital processor hardware and software using SystemC-based virtual prototypes. As a special focus, modeling approaches of instruction-level behavior of System-on-Chips and the connected off-chip digital devices are addressed. Featured verification approaches are based on symbolic execution of simulated hardware devices or on classical discrete execution of the whole system with dynamic data flow tracking. The approaches are accompanied by Case-Studies that develop and build on top of an open-source RISC-V SoC simulation.In Particular, this book:
Formalising Natural Languages: 14th International Conference, NooJ 2020, Zagreb, Croatia, June 5–7, 2020, Revised Selected Papers (Communications in Computer and Information Science #1389)
by Max Silberztein Božo Bekavac Kristina Kocijan Krešimir ŠojatThis book constitutes selected revised papers of the 14th International Conference, NooJ 2020, held Zagreb, Croatia, in June 2020. Due to the COVID-19 pandemic the conference was held online. NooJ is a linguistic development environment that allows linguists to formalize several levels of linguistic phenomena. NooJ provides linguists with tools to develop dictionaries, regular grammars, context-free grammars, context-sensitive grammars and unrestricted grammars as well as their graphical equivalent to formalize each linguistic phenomenon. The 20 full papers presented were carefully reviewed and selected from 68 submissions. The papers are organized in the following topics: Linguistic Formalization; Digital Humanities and Teaching with NooJ; Natural Language Processing Applications.
Formalization of Complex Analysis and Matrix Theory
by Yong Guan Zhiping Shi Ximeng LiThis book discusses the formalization of mathematical theories centering on complex analysis and matrix theory, covering topics such as algebraic systems, complex numbers, gauge integration, the Fourier transformation and its discrete counterpart, matrices and their transformation, inner product spaces, and function matrices. The formalization is performed using the interactive theorem prover HOL4, chiefly developed at the University of Cambridge. Many of the developments presented are now integral parts of the library of this prover.As mathematical developments continue to gain in complexity, sometimes demanding proofs of enormous sizes, formalization has proven to be invaluable in terms of obtaining real confidence in their correctness. This book provides a basis for the computer-aided verification of engineering systems constructed using the principles of complex analysis and matrix theory, as well as building blocks for the formalization of more involved mathematical theories.
Formalizing Data-Centric Web Services
by Iman SalehThis book presents a methodology to model and specify the data aspect of Web services, as it is overlooked by current standards for specifying Web services. The formal specification enables verification of service behavior, and the proposed methodology is based on formal methods and design-by-contract techniques. The Web has evolved from an information sharing medium to a wide-scale environment for sharing capabilities or services. Currently, URLs not only point to documents and images, but are also used to invoke services that potentially change the state of the Web. Major online organizations today, such as Amazon, PayPal and FedEx, provide services for users and consumers. They also allow third-party vendors to resell their services. In both cases, this requires precise and complete specification of service offerings. Several online discussions demonstrate the challenges faced by these organizations and others while describing their data-centric Web services. These challenges surrounding data specification can lead consumers to use a service erroneously. Case studies demonstrate how formal methods, and specifically design-by-contract techniques, can be leveraged to address the lack of formal specification of data when it comes to developing Web applications such as Amazon and PayPal.
Formalizing Natural Languages with NooJ 2018 and Its Natural Language Processing Applications: 12th International Conference, NooJ 2018, Palermo, Italy, June 20–22, 2018, Revised Selected Papers (Communications in Computer and Information Science #987)
by Max Silberztein Mario Monteleone Ignazio Mauro MirtoThis book constitutes the refereed proceedings of the 12th International Conference, NooJ 2018, held in Palermo, Italy, in June 2018. The 17 revised full papers and 3 short papers presented in this volume were carefully reviewed and selected from 48 submissions. NooJ is a linguistic development environment that provides tools for linguists to construct linguistic resources that formalize a large gamut of linguistic phenomena: typography, orthography, lexicons for simple words, multiword units and discontinuous expressions, inflectional and derivational morphology, local, structural and transformational syntax, and semantics. The papers in this volume are organized in topical sections on vocabulary and morphology; syntax and semantics; and natural language processing applications.
Formalizing Natural Languages with NooJ 2019 and Its Natural Language Processing Applications: 13th International Conference, NooJ 2019, Hammamet, Tunisia, June 7–9, 2019, Revised Selected Papers (Communications in Computer and Information Science #1153)
by Max Silberztein Héla Fehri Slim MesfarThis book constitutes the refereed proceedings of the 13th International Conference, NooJ 2019, held in Hammamet, Tunisia, in June 2019. NooJ is a linguistic development environment that allows linguists to formalize several levels of linguistic phenomena. NooJ provides linguists with tools to develop dictionaries, regular grammars, context-free grammars, context-sensitive grammars and unrestricted grammars as well as their graphical equivalent to formalize each linguistic phenomenon. The 18 full papers presented were carefully reviewed and selected from 54 submissions. The papers are organized in the following tracks: Development of Linguistic Resources, Natural Language Processing Applications, NooJ for the Digital Humanities.
Formalizing Natural Languages: 15th International Conference, NooJ 2021, Besançon, France, June 9–11, 2021, Revised Selected Papers (Communications in Computer and Information Science #1520)
by Max Silberztein Magali Bigey Annabel Richeton Izabella ThomasThis book constitutes selected revised papers of the 15th International Conference, NooJ 2021, held in Besançon, France, in June 2021. Due to the COVID-19 pandemic the conference was held online. NooJ is a linguistic development environment that allows linguists to formalize several levels of linguistic phenomena. NooJ provides linguists with tools to develop dictionaries, regular grammars, context-free grammars, context-sensitive grammars and unrestricted grammars as well as their graphical equivalent to formalize each linguistic phenomenon. The 20 full papers presented were carefully reviewed and selected from 62 submissions. The papers are organized in the following topics: linguistic formalization and analysis, digital humanities and teaching, natural language processing applications.
Formalizing Natural Languages: 16th International Conference, NooJ 2022, Rosario, Argentina, June 14–16, 2022, Revised Selected Papers (Communications in Computer and Information Science #1758)
by Max Silberztein Mariana González Silvia Susana Reyes Andrea RodrigoThis book constitutes selected revised papers of the 16th International Conference on Formalizing Natural Languages: Applications to Natural Language Processing and Digital Humanities, NooJ 2022, held in Rosario, Argentina, in June 2022. Due to COVID-19 pandemic the conference was held virtually.NooJ is a linguistic development environment that provides tools for linguists to construct linguistic resources that formalize a large gamut of linguistic phenomena: typography, orthography, lexicons for simple words, multiword units and discontinuous expressions, inflectional, derivational and agglutinative morphology, local, phrase-structure and dependency grammars, as well as transformational and semantic grammars.The 17 full papers presented were carefully reviewed and selected from 50 submissions. The papers are organized in the following topics: Morphological and Lexical Resources; Syntactic and Semantic Resources; Corpus Linguistics and Discourse Analysis; Natural Language Processing Applications.
Formalizing Natural Languages: 17th International Conference, NooJ 2023, Zadar, Croatia, May 31–June 2, 2023, Revised Selected Papers (Communications in Computer and Information Science #1816)
by Max Silberztein Anita Bartulović Linda MijićThis book constitutes the refereed proceedings of the 17th International Conference on Formalizing Natural Languages with NooJ 2023 and Its Natural Language Processing Applications, NooJ 2023, held in Zadar, Croatia, during May 31–June 2, 2023. The 19 full papers included in this book were carefully reviewed and selected from 64 submissions. They were organized in topical sections as follows: morphological and lexical resources; syntactic and semantic resources; corpus linguistics and discourse analysis; and natural language processing applications.
Formalizing Natural Languages: 18th International Conference, NooJ 2024, Bergamo, Italy, June 5–7, 2024, Revised Selected Papers (Communications in Computer and Information Science #2443)
by Max SilberzteinThis book constitutes the refereed proceedings of the 18th International Conference on Automatic Processing of Natural-Language Electronic Texts with NooJ, NooJ 2024, held in Bergamo, Italy, during June 5-7, 2024. The 16 full papers included in this book were carefully reviewed and selected from 64 submissions. These papers have been organized under the following topical sections: Lexical and Morphological Resources; Syntactic Resources; Corpus Linguistics and Discourse Analysis; Natural Language Processing Applications.
Formation Control: Approaches for Distributed Agents (Studies in Systems, Decision and Control #205)
by Hyo-Sung AhnThis monograph introduces recent developments in formation control of distributed-agent systems. Eschewing the traditional concern with the dynamic characteristics of individual agents, the book proposes a treatment that studies the formation control problem in terms of interactions among agents including factors such as sensing topology, communication and actuation topologies, and computations. Keeping pace with recent technological advancements in control, communications, sensing and computation that have begun to bring the applications of distributed-systems theory out of the industrial sphere and into that of day-to-day life, this monograph provides distributed control algorithms for a group of agents that may behave together. Unlike traditional control laws that usually require measurements with respect to a global coordinate frame and communications between a centralized operation center and agents, this book provides control laws that require only relative measurements and communications between agents without interaction with a centralized operator. Since the control algorithms presented in this book do not require any global sensing and any information exchanges with a centralized operation center, they can be realized in a fully distributed way, which significantly reduces the operation and implementation costs of a group of agents. Formation Control will give both students and researchers interested in pursuing this field a good grounding on which to base their work.
Formation and Containment Control for High-order Linear Swarm Systems
by Xiwang DongThis book focuses on analysis and design problems for high-order linear time-invariant (LTI) swarm systems (multi-agent systems) to achieve consensus, formation, containment and formation-containment. As a first step, the concepts of practical consensus and formation-containment are introduced. Unlike previous research, the formation in this book can be time-varying. A general framework for consensus, consensus tracking, formation, containment and state formation-containment is presented for the first time. Sufficient/necessary and sufficient conditions, and approaches to designing the protocols for swarm systems to achieve these control objectives, are respectively proposed. Autonomous time-varying formation experiments using five quadrotor unmanned aerial vehicles (UAVs) are conducted in an outdoor setting to demonstrate the theoretical results.
Forms and Functions of Endings in Narrative Digital Games (Routledge Advances in Game Studies)
by Michelle HerteThis book looks closely at the endings of narrative digital games, examining their ways of concluding the processes of both storytelling and play in order to gain insight into what endings are and how we identify them in different media. While narrative digital games share many representational strategies for signalling their upcoming end with more traditional narrative media – such as novels or movies – they also show many forms of endings that often radically differ from our conventional understanding of conclusion and closure. From vast game worlds that remain open for play after a story’s finale, to multiple endings that are often hailed as a means for players to create their own stories, to the potentially tragic endings of failure and "game over", digital games question the traditional singularity and finality of endings. Using a broad range of examples, this book delves deeply into these and other forms and their functions, both to reveal the closural specificities of the ludonarrative hybrid that digital games are, as well as to find the core elements that characterise endings in any medium. It examines how endings make themselves known to players and raises the question of how well-established closural conventions blend with play and a player’s effort to achieve a goal. As an interdisciplinary study that draws on game studies as much as on transmedial narratology, Forms and Functions of Endings in Narrative Digital Games is suited for scholars and students of digital games as well as for narratologists yet to become familiar with this medium.
Formula 4.0 for Digital Transformation: A Business-Driven Digital Transformation Framework for Industry 4.0
by Venkatesh UpadristaA staggering 70% of digital transformations have failed as per McKinsey. The key reason why enterprises are failing in their digital transformation journey is because there is no standard framework existing in the industry that enterprises can use to transform themselves to digital. There are several books that speak about technologies such as Cloud, Artificial Intelligence and Data Analytics in silos, but none of these provides a holistic view on how enterprises can embark on a digital transformation journey and be successful using a combination of these technologies. FORMULA 4.0 is a methodology that provides clear guidance for enterprises aspiring to transform their traditional operating model to digital. Enterprises can use this framework as a readymade guide and plan their digital transformation journey. This book is intended for all chief executives, software managers, and leaders who intend to successfully lead this digital transformation journey. An enterprise can achieve success in digital transformation only of it can create an IT Platform that will enable them to adopt any new technology seamlessly into existing IT estate; deliver new products and services to the market in shorter durations; make business decisions with IT as an enabler and utilize automation in all its major business and IT processes. Achieving these goals is what defines a digital enterprise -- Formula 4.0 is a methodology for enterprises to achieve these goals and become digital. Essentially, there is no existing framework in the market that provides a step-by-step guide to enterprises on how to embark on their successful digital transformation journey. This book enables such transformations. Overall, the Formula 4.0 is an enterprise digital transformation framework that enables organizations to become truly digital.
Formulating Research Methods for Information Systems
by Leslie P. Willcocks Mary C. Lacity Chris SauerFormulating Research Methods for Information Systems.
Formulating Research Methods for Information Systems: Volume 1
by Leslie P. Willcocks Mary C. Lacity Chris SauerFormulating Research Methods for Information Systems.
Formulating Research Methods for Information Systems: Volume 1
by Leslie P. Willcocks Mary C. Lacity Chris SauerThis edited two-volume collection presents the most interesting and compelling articles pertaining to the formulation of research methods used to study information systems from the 30-year publication history of the Journal of Information Technology .
Formulating Research Methods for Information Systems: Volume 2
by Leslie P. Willcocks Mary C. Lacity Chris SauerThis edited two-volume collection presents the most interesting and compelling articles pertaining to the formulation of research methods used to study information systems from the 30 year publication history of the Journal of Information Technology (JIT).
Forschungsdesigns der Wirtschaftsinformatik: Empfehlungen für die Bachelor- und Masterarbeit (essentials)
by Dominic LindnerIn diesem Buch werden Grundlagen zur empirischen Sozialforschung erläutert und Empfehlungen zur Findung eines Themas für die Abschlussarbeit gegeben. Anschließend werden vier Forschungsdesigns vorgestellt, ergänzt durch Tipps für die Kooperation mit einem Praxispartner. Empfehlungen zum Umgang mit Themen wie Plagiat und Zitierweise runden das Essential ab. Die Inhalte sollen Studierenden aus dem Bereich der Betriebswirtschaft und der Wirtschaftsinformatik als Hilfestellung bei der Konzeption und Erstellung einer Abschlussarbeit dienen.
Forthcoming Networks and Sustainability in the AIoT Era: Second International Conference FoNeS-AIoT 2024 - Volume 1 (Lecture Notes in Networks and Systems #1035)
by Jawad Rasheed Muhammad Fahim Adnan M. Abu-MahfouzThis book introduces a groundbreaking approach to enhancing IoT device security, providing a comprehensive overview of its applications and methodologies. Covering a wide array of topics, from crime prediction to cyberbullying detection, from facial recognition to analyzing email spam, it addresses diverse challenges in contemporary society. Aimed at researchers, practitioners, and policymakers, this book equips readers with practical tools to tackle real-world issues using advanced machine learning algorithms. Whether you're a data scientist, law enforcement officer, or urban planner, this book is a valuable resource for implementing predictive models and enhancing public safety measures. It is a comprehensive guide for implementing machine learning solutions across various domains, ensuring optimal performance and reliability. Whether you're delving into IoT security or exploring the potential of AI in urban landscapes, this book provides invaluable insights and tools to navigate the evolving landscape of technology and data science. The book provides a comprehensive overview of the challenges and solutions in contemporary cybersecurity. Through case studies and practical examples, readers gain a deeper understanding of the security concerns surrounding IoT devices and learn how to mitigate risks effectively. The book's interdisciplinary approach caters to a diverse audience, including academics, industry professionals, and government officials, who seek to address the growing cybersecurity threats in IoT environments. Key uses of this book include implementing robust security measures for IoT devices, conducting research on machine learning algorithms for attack detection, and developing policies to enhance cybersecurity in IoT ecosystems. By leveraging advanced machine learning techniques, readers can effectively detect and mitigate cyber threats, ensuring the integrity and reliability of IoT systems. Overall, this book is a valuable resource for anyone involved in designing, implementing, or regulating IoT devices and systems.