| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996465801403316 |
|
|
Titolo |
ZB 2005: Formal Specification and Development in Z and B [[electronic resource] ] : 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005, Proceedings / / edited by Helen Treharne, Steve King, Martin Henson, Steve Schneider |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2005.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XVI, 496 p.) |
|
|
|
|
|
|
Collana |
|
Programming and Software Engineering ; ; 3455 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computers |
Software engineering |
Computer logic |
Mathematical logic |
Theory of Computation |
Software Engineering |
Logics and Meanings of Programs |
Mathematical Logic and Formal Languages |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Specification Before Satisfaction: The Case for Research into Obtaining the Right Specification —Extended Abstract— -- Visualising Larger State Spaces in Pro B -- Non-atomic Refinement in Z and CSP -- Process Refinement in B -- CZT: A Framework for Z Tools -- Model Checking Z Specifications Using SAL -- Proving Properties of Stateflow Models Using ISO Standard Z and CADiZ -- A Stepwise Development of the Peterson’s Mutual Exclusion Algorithm Using B Abstract Systems -- An Extension of Event B for Developing Grid Systems -- The Challenge of Probabilistic Event B—Extended Abstract— -- Requirements as Conjectures: Intuitive DVD Menu Navigation -- A Prospective-Value Semantics for the GSL -- Retrenchment and the B-Toolkit -- Refinement and Reachability in Event_B -- A Rigorous Foundation for Pattern-Based Design Models -- An Object-Oriented Structuring for Z |
|
|
|
|
|
|
|
|
|
|
Based on Views -- Component Reuse in B Using ACL2 -- GeneSyst: A Tool to Reason About Behavioral Aspects of B Event Specifications. Application to Security Properties -- Formal Verification of a Type Flaw Attack on a Security Protocol Using Object-Z -- Using B as a High Level Programming Language in an Industrial Project: Roissy VAL -- Development via Refinement in Probabilistic B — Foundation and Case Study -- Formal Program Development with Approximations -- Practical Data Refinement for the Z Schema Calculus -- Slicing Object-Z Specifications for Verification -- Checking JML Specifications with B Machines -- Including Design Guidelines in the Formal Specification of Interfaces in Z -- Some Guidelines for Formal Development of Web-Based Applications in B-Method. |
|
|
|
|
|
| |