Automatic Verification Methods for Finite State Systems
Editat de Joseph Sifakisen Limba Engleză Paperback – 10 ian 1990
Preț: 327.07 lei
Preț vechi: 408.84 lei
-20%
Puncte Express: 491
Preț estimativ în valută:
57.84€ • 66.32$ • 49.99£
57.84€ • 66.32$ • 49.99£
Carte tipărită la comandă
Livrare economică 27 aprilie-11 mai
Specificații
ISBN-13: 9783540521488
ISBN-10: 3540521488
Pagini: 396
Ilustrații: XI, 384 p.
Dimensiuni: 155 x 235 x 22 mm
Greutate: 0.6 kg
Ediția:1990
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540521488
Pagini: 396
Ilustrații: XI, 384 p.
Dimensiuni: 155 x 235 x 22 mm
Greutate: 0.6 kg
Ediția:1990
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Process calculi, from theory to practice: Verification tools.- Testing equivalence as a bisimulation equivalence.- The concurrency workbench.- Argonaute: Graphical description, semantics and verification of reactive systems by using a process algebra.- Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications.- Verifying properties of large sets of processes with network invariants.- A method for verification of trace and test equivalence.- Projections of the reachability graph and environment models.- Proving properties of elementary net systems with a special-purpose theorem prover.- Verification by abstraction and bisimulation.- MEC : a system for constructing and analysing transition systems.- Fair SMG and linear time model checking.- Network grammars, communication behaviors and automatic verification.- CCS, liveness, and local model checking in the linear time mu-calculus.- Implementing a model checking algorithm by adapting existing automated tools.- On-line model-checking for finite linear temporal logic specifications.- Timing assumptions and verification of finite-state concurrent systems.- Specifying, programming and verifying real-time systems using a synchronous declarative language.- Modal specifications.- Automated verification of timed transition models.- Temporal logic case study.- The complexity of collapsing reachability graphs.- What are the limits of model checking methods for the verification of real life protocols?.- Requirement analysis for communication protocols.- State exploration by transformation with lola.- Parallel protocol verification: The two-phase algorithm and complexity analysis.- Formal verification of synchronous circuits based on string-functional semantics: The 7 paillet circuits in boyer-moore.- Combining CTL, trace theory and timing models.- Localized verification of circuit descriptions.- Verification of synchronous sequential machines based on symbolic execution.- Parallel composition of lockstep synchronous processes for hardware validation: Divide-and-conquer composition.