Edizione	[1st ed. 2008.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008
Descrizione fisica	1 online resource (VII, 234 p.)
Disciplina	005.131
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Software engineering Compilers (Computer programs) Computer science Computer programming Machine theory Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming Programming Techniques Formal Languages and Automata Theory
ISBN	3-540-69850-7
Classificazione	DAT 003f DAT 325f DAT 540f SS 4800
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	The Birth of Model Checking -- The Beginning of Model Checking: A Personal Perspective -- Verification Technology Transfer -- New Challenges in Model Checking -- A Retrospective on Mur? -- Model Checking: From Tools to Theory -- Value Iteration -- Fifteen Years of Formal Property Verification in Intel -- A View from the Engine Room: Computational Support for Symbolic Model Checking -- From Church and Prior to PSL -- On the Merits of Temporal Testers -- DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC -- SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR.
Record Nr.	UNISA-996465393403316

Edizione	[1st ed. 2010.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica	1 online resource (XIV, 416 p. 95 illus.)
Disciplina	004.0151
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Computer science Machine theory Algorithms Computer science—Mathematics Theory of Computation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Mathematics of Computing
ISBN	1-280-38571-5 9786613563637 3-642-11811-9
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Invited Talks -- A Structure for Dependability Arguments -- Formal Probabilistic Analysis: A Higher-Order Logic Based Approach -- ASM Papers -- Synchronous Message Passing and Semaphores: An Equivalence Proof -- AsmL-Based Concurrency Semantic Variations for Timed Use Case Maps -- Bârun: A Scripting Language for CoreASM -- AsmetaSMV: A Way to Link High-Level ASM Models to Low-Level NuSMV Specifications -- An Executable Semantics of the SystemC UML Profile -- Alloy Papers -- Specifying Self-configurable Component-Based Systems with FracToy -- Trace Specifications in Alloy -- An Imperative Extension to Alloy -- Towards Formalizing Network Architectural Descriptions -- Lightweight Modeling of Java Virtual Machine Security Constraints -- Alloy+HotCore: A Fast Approximation to Unsat Core -- B Papers -- Supporting Reuse in Event B Development: Modularisation Approach -- Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance -- Applying the B Method for the Rigorous Development of Smart Card Applications -- Automatic Verification for a Class of Proof Obligations with SMT-Solvers -- A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking -- Development of a Synchronous Subset of AADL -- Matelas: A Predicate Calculus Common Formal Definition for Social Networking -- Structured Event-B Models and Proofs -- Refinement-Animation for Event-B — Towards a Method of Validation -- Reactivising Classical B -- Event-B Decomposition for Parallel Programs -- Z Papers -- Communication Systems in ClawZ -- Formalising and Validating RBAC-to-XACML Translation Using Lightweight Formal Methods -- Towards Formally Templated Relational Database Representations in Z -- Translating Z to Alloy -- ABZ Short Papers (Abstracts) -- B-ASM: Specification of ASM à la B -- A Case for Using Data-Flow Analysis to Optimize Incremental Scope-Bounded Checking -- On the Modelling and Analysis of Amazon Web Services Access Policies -- Architecture as an Independent Variable for Aspect-Oriented Application Descriptions -- ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models -- Introducing Specification-Based Data Structure Repair Using Alloy -- Secrecy UML Method for Model Transformations -- Improving Traceability between KAOS Requirements Models and B Specifications -- Code Synthesis for Timed Automata: A Comparison Using Case Study -- Towards Validation of Requirements Models -- A Proof Based Approach for Formal Verification of Transactional BPEL Web Services -- On an Extensible Rule-Based Prover for Event-B -- B Model Abstraction Combining Syntactic and Semantic Methods -- A Basis for Feature-Oriented Modelling in Event-B -- Using Event-B to Verify the Kmelia Components and Their Assemblies -- Starting B Specifications from Use Cases -- Integrating SMT-Solvers in Z and B Tools -- Formal Analysis in Model Management: Exploiting the Power of CZT.
Record Nr.	UNISA-996465641803316

Edizione	[1st ed. 2018.]
Pubbl/distr/stampa	Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018
Descrizione fisica	1 online resource (XIV, 432 p. 83 illus.)
Disciplina	006.31
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Machine theory Algorithms Computer science Compilers (Computer programs) Artificial intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Compilers and Interpreters Artificial Intelligence
ISBN	3-319-91271-2
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Invited Talks -- Translation and Transformation -- Analysis and Tests -- Reals and Hybrid Systems -- Refinement -- Hybrid ERTMS Case Study -- Short Papers.
Record Nr.	UNISA-996465825303316

Edizione	[1st ed. 2016.]
Pubbl/distr/stampa	Cham : , : Springer International Publishing : , : Imprint : Springer, , 2016
Descrizione fisica	1 online resource (XXI, 426 p. 143 illus.)
Disciplina	004
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Machine theory Computer science Software engineering Compilers (Computer programs) Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Theory of Computation Software Engineering Compilers and Interpreters
ISBN	3-319-33600-2
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets -- A Universal Control Construct for Abstract State Machines -- Encoding TLA+ into Many-Sorted First-Order Logic -- Proving Determinacy of PharOS in TLA+ -- A Rigorous Correctness Proof for Pastry -- Enabling Analysis for B and Event-B -- A Compact Encoding of Sequential ASMs in Event-B -- Proof Assisted Symbolic Model Checking for B and Event-B -- On Component-based Reuse for Event-B -- Using B and ProB for Data Validation Projects -- Generating Event-B Specifications from Algorithm Descriptions -- Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions -- How to Select the Suitable Formal Method for an Industrial Application: A Survey -- Unified Syntax for Abstract State Machines -- A Relational Encoding for a Clash-Free Subset of ASMs -- Towards an ASM Thesis for Reflective Sequential Algorithms -- A Model-based Transformation Approach to Reuse and Retarget CASM Specifications -- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy -- `The Tinker' for Rodin -- A Graphical Tool for Event Refinement Structures in Event-B -- Rodin Platform Why3 plug-in -- Semi-Automated Design Space Exploration for Formal Modelling -- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development -- UC-B: Use Case Modelling with Event-B -- Interactive Model Repair by Synthesis -- SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML -- Mechanized Refinement of Communication Models with TLA+ -- A Super Industrial Application of PSGraph -- The Hemodialysis Machine Case Study -- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study -- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation -- Hemodialysis Machine in Hybrid Event-B -- Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods -- Modelling the Haemodialysis Machine with Circus.
Record Nr.	UNISA-996465777503316

Edizione	[1st ed. 2014.]
Pubbl/distr/stampa	Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2014
Descrizione fisica	1 online resource (XVI, 336 p. 93 illus.)
Disciplina	005.131
Collana	Theoretical Computer Science and General Issues
Soggetto topico	Machine theory Computer science Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Theory of Computation
ISBN	3-662-43652-3
Formato	Materiale a stampa
Livello bibliografico	Monografia
Lingua di pubblicazione	eng
Nota di contenuto	Fundamental contributions -- Applications in industrial contexts -- Tool developments and improvements.
Record Nr.	UNISA-996217774103316