Cantitate/Preț
Produs
Total produse
Vezi coșul
Formal Methods and Software Engineering: 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings de Jin Song Dong

Formal Methods and Software Engineering: 12th International Conference on Formal Engineering Methods, ICFEM 2010, Shanghai, China, November 17-19, 2010, Proceedings: Lecture Notes in Computer Science, cartea 6447

Editat de Jin Song Dong, Huibiao Zhu
en Limba Engleză Paperback – 29 oct 2010

Dincolo de documentația oficială a limbajelor de programare, volumul Formal Methods and Software Engineering oferă o perspectivă analitică asupra modului în care conceptele matematice riguroase pot fi integrate în ciclul de dezvoltare software. Spre deosebire de manualele teoretice, această colecție de lucrări de la conferința ICFEM 2010 se concentrează pe aplicabilitatea metodelor formale în scenarii reale, precum sistemele embedded multicore sau compoziția serviciilor web. Abordarea diferă de Fundamentals of Software Engineering de Farhad Arbab prin faptul că este mai puțin abstractă și mult mai aplicabilă, punând accent pe generarea și descărcarea obligațiilor de probă pentru definiții recursive în VDM sau pe strategii de demonstrare în programarea bazată pe invarianți. Remarcăm o structură riguroasă, organizată pe paliere de complexitate crescătoare: de la demonstrarea teoremelor și proceduri de decizie, până la studiul fluxurilor de lucru compensabile și analiza performanței prin ecuații diferențiale. Editorul Jin Song Dong, cunoscut pentru versatilitatea sa în coordonarea publicațiilor de cercetare — de la Semantic Technology până la volume recente despre Sports Analytics — menține aici un standard ridicat de rigoare academică aplicată. Descoperim în paginile sale soluții pentru verificarea programelor care manipulează heap-ul și modele semantice pentru coordonarea serviciilor cu întârzieri temporale, oferind instrumente concrete pentru inginerii software care urmăresc corectitudinea prin construcție.

Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 64145 lei

Preț vechi: 80181 lei
-20%

Puncte Express: 962

Carte disponibilă

Livrare economică 27 mai-10 iunie

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă

Specificații

ISBN-13: 9783642169007
ISBN-10: 3642169007
Pagini: 712
Ilustrații: XIV, 712 p. 202 illus.
Greutate: 1.02 kg
Ediția:2010
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Programming and Software Engineering

Locul publicării:Berlin, Heidelberg, Germany

Public țintă

Research

De ce să citești această carte

Recomandăm această lucrare cercetătorilor și inginerilor software care doresc să treacă de la testarea empirică la verificarea formală a sistemelor complexe. Cititorul câștigă acces la studii de caz avansate despre model checking și analiza programelor, fundamentale pentru dezvoltarea de software critic unde siguranța și corectitudinea sunt imperative.

Descriere scurtă

This book constitutes the refereed proceedings of the 12th International
Conference on Formal Engineering Methods, ICFEM 2010, held in Shanghai, China,
November 2010.

The 42 revised full papers together with 3 invited talks presented were carefully reviewed and selected from 114 submissions. The papers address all current issues in formal methods and their applications in software engineering. They are organized in topical sections on theorem proving and decision procedures, web services and workflow, verification, applications of formal methods, probability and concurrency, program analysis, model checking, object orientation and mod
el driven engineering, as well as specification and verification.

Cuprins

Invited Talks.- Fostering Proof Scores in CafeOBJ.- Exploiting Partial Success in Applying Automated Formal Methods.- Multicore Embedded Systems: The Timing Problem and Possible Solutions.- Theorem Proving and Decision Procedures.- Applying PVS Background Theories and Proof Strategies in Invariant Based Programming.- Proof Obligation Generation and Discharging for Recursive Definitions in VDM.- Correct-by-Construction Model Transformations from Partially Ordered Specifications in Coq.- Decision Procedures for the Temporal Verification of Concurrent Lists.- An Improved Decision Procedure for Propositional Projection Temporal Logic.- Web Services and Workflow.- A Semantic Model for Service Composition with Coordination Time Delays.- Compensable WorkFlow Nets.- Automatically Testing Web Services Choreography with Assertions.- Applying Ordinary Differential Equations to the Performance Analysis of Service Composition.- Verification I.- Verifying Heap-Manipulating Programs with Unknown Procedure Calls.- API Conformance Verification for Java Programs.- Assume-Guarantee Reasoning with Local Specifications.- Automating Coinduction with Case Analysis.- Applications of Formal Methods.- Enhanced Semantic Access to Formal Software Models.- Making Pattern- and Model-Based Software Development More Rigorous.- Practical Parameterised Session Types.- A Formal Verification Study on the Rotterdam Storm Surge Barrier.- Verification II.- Formalization and Correctness of the PALS Architectural Pattern for Distributed Real-Time Systems.- Automated Multiparameterised Verification by Cut-Offs.- Automating Cut-off for Multi-parameterized Systems.- Method for Formal Verification of Soft-Error Tolerance Mechanisms in Pipelined Microprocessors.- Formal Verification of Tokeneer Behaviours Modelled in fUML Using CSP.- Probability and Concurrency.- Model Checking Hierarchical Probabilistic Systems.- Trace-Driven Verification of Multithreaded Programs.- Closed Form Approximations for Steady State Probabilities of a Controlled Fork-Join Network.- Reasoning about Safety and Progress Using Contracts.- Program Analysis.- Abstract Program Slicing: From Theory towards an Implementation.- Loop Invariant Synthesis in a Combined Domain.- Software Metrics in Static Program Analysis.- A Combination of Forward and Backward Reachability Analysis Methods.- Model Checking.- Model Checking a Model Checker: A Code Contract Combined Approach.- On Symmetries and Spotlights – Verifying Parameterised Systems.- A Methodology for Automatic Diagnosability Analysis.- Making the Right Cut in Model Checking Data-Intensive Timed Systems.- Comparison of Model Checking Tools for Information Systems.- Object Orientation and Model Driven Engineering.- A Modular Scheme for Deadlock Prevention in an Object-Oriented Programming Model.- Model-Driven Protocol Design Based on Component Oriented Modeling.- Laws of Pattern Composition.- Dynamic Resource Reallocation between Deployment Components.- Specification and Verification.- A Pattern System to Support Refining Informal Ideas into Formal Expressions.- Specification Translation of State Machines from Equational Theories into Rewrite Theories.- Alternating Interval Based Temporal Logics.