Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Abstract state machines, Alloy B and Z : second international conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010 : proceedings / / Marc Frappier ... [et al.] (eds.)
| Abstract state machines, Alloy B and Z : second international conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010 : proceedings / / Marc Frappier ... [et al.] (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer-Verlag, c2010 |
| Descrizione fisica | 1 online resource (XIV, 416 p. 95 illus.) |
| Disciplina | 004.0151 |
| Altri autori (Persone) | FrappierMarc <1965-> |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Machine theory
B method (Computer science) Z (Computer program language) |
| 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. | UNINA-9910483437903321 |
| Berlin ; ; Heidelberg, : Springer-Verlag, c2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Refinement in Z and object-Z : foundations and advanced applications / / John Derrick, Eerke A. Boiten
| Refinement in Z and object-Z : foundations and advanced applications / / John Derrick, Eerke A. Boiten |
| Autore | Derrick John |
| Edizione | [2nd ed.] |
| Pubbl/distr/stampa | New York, : Springer, 2014 |
| Descrizione fisica | 1 online resource (xviii, 492 pages) : illustrations |
| Disciplina | 005.13/3 |
| Altri autori (Persone) | BoitenEerke A |
| Collana | Gale eBooks |
| Soggetto topico | Z (Computer program language) |
| ISBN | 1-4471-5355-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | pt. I. Refining Z specifications -- pt. II. Interfaces and operations : ADTs viewed in an environment -- pt. III. Object-oriented refinement -- pt. IV. Modelling state and behaviour. |
| Record Nr. | UNINA-9910298981503321 |
Derrick John
|
||
| New York, : Springer, 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
ZB 2005 : formal specification and development in Z and B : 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005 : proceedings / / Helen Treharne ... [et al.] (eds.)
| ZB 2005 : formal specification and development in Z and B : 4th International Conference of B and Z Users, Guildford, UK, April 13-15, 2005 : proceedings / / Helen Treharne ... [et al.] (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2005 |
| Descrizione fisica | 1 online resource (XVI, 496 p.) |
| Disciplina | 005.133 |
| Altri autori (Persone) | TreharneHelen |
| Collana | Lecture notes in computer science |
| Soggetto topico |
B (Computer program language)
Z (Computer program language) |
| ISBN | 3-540-32007-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| 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. |
| Record Nr. | UNINA-9910483494203321 |
| Berlin ; ; New York, : Springer, 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Zum'98 : the z formal specification notation : 11th international conference of z users, berlin, germany, september 24-26, 1998 : proceedings / / edited by Jonathan P. Bowen, Andreas Fett, Michael G. Hinchey
| Zum'98 : the z formal specification notation : 11th international conference of z users, berlin, germany, september 24-26, 1998 : proceedings / / edited by Jonathan P. Bowen, Andreas Fett, Michael G. Hinchey |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [1998] |
| Descrizione fisica | 1 online resource (XVI, 424 p.) |
| Disciplina | 005.133 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Z (Computer program language) |
| ISBN | 3-540-49676-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Industrial Issues -- Industrial Requirements for the Efficient Development of Reliable Embedded Systems -- Concurrency -- How to Combine Z with a Process Algebra -- The Specification and Refinement of an Environmental Model -- Formal Derivation of Finite State Machines for Class Testing -- Tools -- Using B to Specify, Verify and Design Hardware Circuits -- Z on the Web Using Java -- Visualizing Z Notation in HTML Documents -- Z and HOL -- On the Semantic Relation of Z and HOL -- HOL-Z in the UniForM-Workbench – A Case Study in Tool Integration for Z -- Safety-Critical and Real-Time Systems -- Designing a Requirements Specification Language for Reactive Systems -- Analyzing a Real-Time Program with Z -- Semantic Theory -- Recursive Definitions in Z -- A Logic for the Schema Calculus -- Theory and Standards -- Combining Specification Techniques for Processes, Data and Time -- Innovations in the Notation of Standard Z -- Reasoning and Consistency Issues -- Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space -- Inconsistency and Undefinedness in Z – A Practical Guide -- Refinement -- Compositional Specification of Controllers for Batch Process Operations -- Testing Refinements by Refining Tests -- More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement -- Object Orientation -- Network Topology and a Case Study in TCOZ -- Object-Oriented Specification of Hybrid Systems Using UML h and ZimOO -- Translating the OMT Dynamic Model into Object-Z -- Appendices -- Select Z Bibliography -- Comp.specification.z and Z FORUM Frequently Asked Questions. |
| Record Nr. | UNISA-996466141203316 |
| Berlin, Germany : , : Springer, , [1998] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Zum'98 : the z formal specification notation : 11th international conference of z users, berlin, germany, september 24-26, 1998 : proceedings / / edited by Jonathan P. Bowen, Andreas Fett, Michael G. Hinchey
| Zum'98 : the z formal specification notation : 11th international conference of z users, berlin, germany, september 24-26, 1998 : proceedings / / edited by Jonathan P. Bowen, Andreas Fett, Michael G. Hinchey |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [1998] |
| Descrizione fisica | 1 online resource (XVI, 424 p.) |
| Disciplina | 005.133 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Z (Computer program language) |
| ISBN | 3-540-49676-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Industrial Issues -- Industrial Requirements for the Efficient Development of Reliable Embedded Systems -- Concurrency -- How to Combine Z with a Process Algebra -- The Specification and Refinement of an Environmental Model -- Formal Derivation of Finite State Machines for Class Testing -- Tools -- Using B to Specify, Verify and Design Hardware Circuits -- Z on the Web Using Java -- Visualizing Z Notation in HTML Documents -- Z and HOL -- On the Semantic Relation of Z and HOL -- HOL-Z in the UniForM-Workbench – A Case Study in Tool Integration for Z -- Safety-Critical and Real-Time Systems -- Designing a Requirements Specification Language for Reactive Systems -- Analyzing a Real-Time Program with Z -- Semantic Theory -- Recursive Definitions in Z -- A Logic for the Schema Calculus -- Theory and Standards -- Combining Specification Techniques for Processes, Data and Time -- Innovations in the Notation of Standard Z -- Reasoning and Consistency Issues -- Comparing Extended Z with a Heterogeneous Notation for Reasoning about Time and Space -- Inconsistency and Undefinedness in Z – A Practical Guide -- Refinement -- Compositional Specification of Controllers for Batch Process Operations -- Testing Refinements by Refining Tests -- More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement -- Object Orientation -- Network Topology and a Case Study in TCOZ -- Object-Oriented Specification of Hybrid Systems Using UML h and ZimOO -- Translating the OMT Dynamic Model into Object-Z -- Appendices -- Select Z Bibliography -- Comp.specification.z and Z FORUM Frequently Asked Questions. |
| Record Nr. | UNINA-9910768472503321 |
| Berlin, Germany : , : Springer, , [1998] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
