Edizione	[1st ed. 2020.]
Pubbl/distr/stampa	Cham, Switzerland : , : Springer, , [2020]
Descrizione fisica	1 online resource (XIII, 203 p. 228 illus., 31 illus. in color.)
Disciplina	005.1
Collana	Programming and Software Engineering
Soggetto topico	Formal methods (Computer science) Computers Software engineering
ISBN	3-030-62822-1
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	The Road Ahead for Supervisor Synthesis -- Reentrancy? Yes. Reentrancy bug? No -- Graph Transformation Systems: a Semantics Based on (Stochastic) Symmetric Nets -- Modelling and Implementation of Unmanned Aircraft Collision Avoidance -- Randomized Re nement Checking of Timed I/O Automata -- Computing Linear Arithmetic Representation for Reachability Relation of One-counter Automata -- Compiling FL^{res} on Finite Words -- Symbolic Model Checking with Sentential Decision Diagrams -- Probably Approximately Correct Interpolants Generation -- Symbolic Verification of MPI Programs with Non-deterministic Synchronizations -- Learning Safe Neural Network Controllers with Barrier Certificates -- Software Defect-proneness Prediction Based on Package Cohesion and Coupling Metrics.
Record Nr.	UNISA-996418222403316

Pubbl/distr/stampa	Piscataway, New Jersey : , : Institute of Electrical and Electronics Engineers, , 2017
Descrizione fisica	1 online resource (890 pages)
Disciplina	004.0151
Soggetto topico	Formal methods (Computer science) Software engineering
Soggetto genere / forma	Electronic books.
ISBN	1-5386-4733-8
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Record Nr.	UNISA-996279512103316

Pubbl/distr/stampa	New York : , : IEEE, , 2015
Descrizione fisica	1 online resource (333 pages)
Soggetto topico	Formal methods (Computer science) Software engineering Computer software - Verification
ISBN	979-1-0922-7904-7 2-9530504-9-3
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Record Nr.	UNISA-996279792503316

Edizione	[1st ed. 1999.]
Pubbl/distr/stampa	Berlin : , : Springer, , [1999]
Descrizione fisica	1 online resource (XXXVI, 940 p.)
Disciplina	005.131
Collana	Lecture Notes in Computer Science
Soggetto topico	Application software - Development Formal methods (Computer science)
ISBN	3-540-48119-2
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Invited Papers -- Theories of Programming: Top-Down and Bottom-Up and Meeting in the Middle -- Scientific Decisions which Characterize VDM -- Mechanized Formal Methods: Where Next? -- Integration, the Price of Success -- The Role of Formalism in Method -- Integration into the Development Process -- Formal Design for Automatic Coding and Testing: The ESSI/SPACES Project -- A Business Process Design Language -- Software Architecture -- Refinement of Pipe-and-Filter Architectures -- A Formalization of Software Architecture -- European Association for Theoretical Computer Science (EATCS) -- Component and Interface Refinement in Closed-System Specifications -- Semantics of First Order Parametric Specifications -- Model Checking -- A Perfecto Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software -- Error Detection with Directed Symbolic Model Checking -- Formal Modeling and Analysis of Hybrid Systems: A Case Study in Multi-robot Coordination -- On-the-Fly Controller Synthesis for Discrete and Dense-Time Systems -- On-the-fly Verification of Linear Temporal Logic -- Symbolic Model Checking with Fewer Fixpoint Computations -- Formula Based Abstractions of Transition Systems for Real-Time Model Checking -- If: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems -- Automatic Verification of Pointer Data-Structure Systems for All Numbers of Processes -- The B Method -- The Use of the B Formal Method for the Design and the Validation of the Transaction Mechanism for Smart Card Applications -- Météor: A Successful Application of B in a Large Project -- Formal Development of Databases in ASSO and B -- Interpreting the B-Method in the Refinement Calculus -- Compositional Symmetric Sharing in B -- Structural Embeddings: Mechanization with Method -- The Safe Machine: A New Specification Construct for B -- csp2B: A Practical Approach to Combining CSP and B -- Test Criteria Definition for B Models -- Composition and Synthesis -- Bunches for Object-Oriented, Concurrent, and Real-Time Specification -- Applications of Structural Synthesis of Programs -- Towards a Compositional Approach to the Design and Verification of Distributed Systems -- Telecommunications -- Formal Modeling in a Commercial Setting: A Case Study -- KVEST: Automated Generation of Test Suites from Formal Specifications -- Feature Interaction Detection Using Testing and Model-Checking Experience Report -- Emma: Developing an Industrial Reachability Analyser for SDL -- Correctness Proof of the Standardized Algorithm for ABR Conformance -- Verifying a Distributed Database Lookup Manager Written in Erlang -- Security -- Secure Interoperation of Secure Distributed Databases -- A Formal Security Model for Microprocessor Hardware -- Abstraction and Testing -- Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol -- Probabilistic Polynomial-Time Equivalence and Security Analysis -- A Uniform Approach for the Definition of Security Properties -- Group Principals and the Formalization of Anonymity -- Object-Orientation -- Developing BON as an Industrial-Strength Formal Method -- On the Expressive Power of OCL -- A Systematic Approach to Transform OMT Diagrams to a B Specification -- Verifying Consistency and Validity of Formal -- Verifying Consistency and Validity of Formal Specifications by Testing -- A GSM-MAP Protocol Experiment Using Passive Testing.
Altri titoli varianti	Formal methods
Record Nr.	UNISA-996465302703316

Edizione	[1st ed. 1999.]
Pubbl/distr/stampa	Berlin, Germany ; ; New York, New York : , : Springer, , [1999]
Descrizione fisica	1 online resource (XVIII, 942 p.)
Disciplina	005.131
Collana	Lecture Notes in Computer Science
Soggetto topico	Application software - Development Formal methods (Computer science)
ISBN	3-540-48118-4
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Foundations of System Specification (IFIP WG 1.3) -- From informal requirements to COOP: a concurrent automata approach -- A framework for defining Object-Calculi extended abstract -- European Theory and Practice of Software (ETAPS) -- A translation of statecharts to esterel -- An operational semantics for timed RAISE -- Data abstraction for CSP-OZ -- Systems development using Z generics -- A brief summary of VSPEC -- Enhancing the pre- and postcondition technique for more expressive specifications -- Program Verification -- On excusable and inexcusable failures towards an adequate notion of translation correctness -- Interfacing program construction and verification -- Software verification based on linear programming -- Integration of Notation and Techniques -- Sensors and actuators in TCOZ -- The UniForM workbench a universal development environment for formal methods -- Integrating formal description techniques -- Formal Description of Programming Concepts (IFIP WG 2.2) -- A more complete TLA -- Formal justification of the rely-guarantee paradigm for shared-variable concurrency: a semantic approach -- Relating Z and first-order logic -- Open Information Systems -- Formal modeling of the enterprise javabeans™ component integration framework -- Developing components in the presence of re-entrance -- Communication and synchronisation using interaction objects -- Modelling microsoft COM using ?-calculus -- Co-design -- Validation of mixed signal-alpha real-time systems through affine calculus on clock synchronisation constraints -- Combining theorem proving and continuous models in synchronous design -- Parts a partitioning transformation system -- A behavioral model for co-design -- Refinement -- A weakest precondition semantics for an object-oriented language of refinement -- Reasoning about interactive systems -- Non-atomic refinement in Z -- Refinement semantics and loop rules -- Safety -- Lessons from the application of formal methods to the design of a storm surge barrier control system -- The value of verification: positive experience of Industrial proof -- Formal development and verification of a distributed railway control system -- Safety analysis in formal specication -- Formal specification and validation of a vital communication protocol -- Incremental design of a Power transformer station controller using a controller synthesis methodology -- OBJ/Cafe OBJ/Maude -- Verifying behavioural specifications in CafeOBJ environment -- Component-based algebraic specification and verification in cafeOBJ -- Using algebraic specification techniques in development of object-oriented frameworks -- Maude as a formal meta-tool -- Hiding more of hidden algebra -- Abstract State Machines (ASM) and Algebraic Methods in Software Technology (AMAST) -- A termination detection algorithm: specification and verification -- Logspace reducibility via abstract state machines -- Formal methods for extensions to CAS -- An lgebraic framework for higher-order odules -- Avionics -- Applying formal proof techniques to avionics software: a pragmatic approach -- Secure synthesis of code: a process improvement experiment -- Cronos: a separate compilation tool set for modular esterel applications -- Works-in-Progress -- Tool support for production use of formal techniques -- Modeling aircraft mission computer task rates -- A study of collaborative work: answers to a test on formal specification in B -- Archived design steps in temporal logic -- A PVS-based approach for teaching constructing correct iterations -- A minimal framework for specification theory -- A model of specification-based testing of interactive systems -- Algebraic aspects of the mapping between abstract syntax notation one and CORBA IDL -- Retrenchment -- Proof preservation in component generalization -- Industrial Experience -- Formal modelling and simulation of train control systems using petri nets -- Formal specification of a voice communication system used in air traffic control an industrial application of light-weight formal methods using vdm -- Model-checking the architectural design of a fail-safe communication system for railway interlocking systems -- Analyzing the requirements of an access control using VDMTools and PVS -- Cache coherence verification with TLA%.
Altri titoli varianti	Formal methods
Record Nr.	UNISA-996465304103316