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, VDM, and Z [[electronic resource] ] : Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings / / edited by John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene
| Abstract State Machines, Alloy, B, VDM, and Z [[electronic resource] ] : Third International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings / / edited by John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XV, 378 p. 133 illus.) |
| Disciplina | 006.3/1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Algorithms Computer science—Mathematics Discrete mathematics Computer Science Logic and Foundations of Programming Theory of Computation Mathematics of Computing Discrete Mathematics in Computer Science |
| ISBN | 3-642-30885-6 |
| Classificazione | 54.53 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Contribution to a Rigorous Analysis of Web Application Frameworks / Egon Börger, Antonio Cisternino and Vincenzo Gervasi -- Integrated Operational Semantics: Small-Step, Big-Step and Multi-step / Ian J. Hayes and Robert J. Colvin -- Test Generation for Sequential Nets of Abstract State Machines / Paolo Arcaini, Francesco Bolis and Angelo Gargantini -- ASM and Controller Synthesis / Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu -- Continuous ASM, and a Pacemaker Sensing Fragment / Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu -- An ASM Model of Concurrency in a Web Browser / Vincenzo Gervasi -- Modeling the Supervisory Control Theory with Alloy / Benoît Fraikin, Marc Frappier and Richard St-Denis -- Preventing Arithmetic Overflows in Alloy / Aleksandar Milicevic and Daniel Jackson -- Extending Alloy with Partial Instances / Vajih Montaghami and Derek Rayside -- Toward a More Complete Alloy / Timothy Nelson, Daniel J. Dougherty, Kathi Fisler and Shriram Krishnamurthi -- Temporal Logic Model Checking in Alloy / Amirhossein Vakili and Nancy A. Day -- Active Attacking Multicast Key Management Protocol Using Alloy / Ting Wang and Dongyao Ji -- Formalizing Hybrid Systems with Event-B / Jean-Raymond Abrial, Wen Su and Huibiao Zhu -- SMT Solvers for Rodin / David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin -- Refinement Plans for Informed Formal Design / Gudmund Grov, Andrew Ireland and Maria Teresa Llano -- Refinement by Interface Instantiation / Stefan Hallerstede and Thai Son Hoang -- Discharging Proof Obligations from Atelier B Using Multiple Automated Provers / David Mentré, Claude Marché, Jean-Christophe Filliâtre and Masashi Asuka -- A Semantic Analysis of Logics That Cope with Partial Terms / Cliff B. Jones, Matthew J. Lovert and L. Jason Steggles -- Combining VDM with Executable Code / Claus Ballegaard Nielsen, Kenneth Lausdahl and Peter Gorm Larsen -- Extending the Test Template Framework to Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions / Maximiliano Cristiá and Claudia Frydman -- A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams / Chris Marriott, Frank Zeyda and Ana Cavalcanti -- Verification of Hardware Interaction Properties of Software / Ramsay Taylor -- Using the Arbitrator Pattern for Dynamic Process-Instance Extension in a Work-Flow Management System / Matthes Elstermann, Detlef Seese and Albert Fleischmann -- A Unified Processor Model for Compiler Verification and Simulation Using ASM / Roland Lezuo and Andreas Krall -- Modeling Synchronization/Communication Patterns in Vision-Based Robot Control Applications Using ASMs / Andrea Luzzana, Mattia Rossetti, Paolo Righettini and Patrizia Scandurra -- A Reliability Prediction Method for Abstract State Machines / Raffaela Mirandola, Pasqualina Potena and Patrizia Scandurra -- A Simplified Parallel ASM Thesis / Klaus-Dieter Schewe and Qing Wang -- Refactoring Abstract State Machine Models / Hamed Yaghoubi Shahir, Roozbeh Farahbod and Uwe Glässer -- Continuous Behaviour in Event-B: A Sketch / Richard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu -- Formal Verification of PLC Programs Using the B Method / Haniel Barbosa and David Déharbe -- A Practical Event-B Refinement Method Based on a UML-Driven Development Process / Thiago C. de Sousa, Paulo Sérgio Muniz Silva and Colin F. Snook -- Learn and Test for Event-B -- A Rodin Plugin / Ionut Dinca, Florentin Ipate, Laurentiu Mierla and Alin Stefanescu -- Event-B Code Generation: Type Extension with Theories / Andrew Edmunds, Michael Butler, Issam Maamria, Renato Silva and Chris Lovell -- Formal Proofs for the NYCT Line 7 (Flushing) Modernization Project / Denis Sabatier, Lilian Burdy, Antoine Requet and Jérôme Guéry -- A Pattern for Modelling Fault Tolerant Systems in Event-B / Gintautas Sulskus and Michael Poppleton. |
| Record Nr. | UNISA-996465312903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
FM 2005: Formal Methods [[electronic resource] ] : International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings / / edited by John Fitzgerald, Ian J. Hayes
| FM 2005: Formal Methods [[electronic resource] ] : International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings / / edited by John Fitzgerald, Ian J. Hayes |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XIV, 558 p.) |
| Disciplina | 004.13/1 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Computer logic Programming languages (Electronic computers) Computer programming Mathematical logic Management information systems Computer science Software Engineering Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Programming Techniques Mathematical Logic and Formal Languages Management of Computing and Information Systems |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Keynote Talks -- Formal Aids for the Growth of Software Systems -- Formal Methods and Testing: Hypotheses, and Correctness Approximations -- The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions -- Object Orientation -- Modular Verification of Static Class Invariants -- Decoupling in Object Orientation -- Controlling Object Allocation Using Creation Guards -- Symbolic Animation of JML Specifications -- Resource Analysis and Verification -- Certified Memory Usage Analysis -- Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs -- Formally Defining and Verifying Master/Slave Speculative Parallelization -- Timing and Testing -- Systematic Implementation of Real-Time Models -- Timing Tolerances in Safety-Critical Software -- Timed Testing with TorX -- Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems -- CSP, B and Circus -- Adding Conflict and Confusion to CSP -- Combining CSP and B for Specification and Property Verification -- Operational Semantics for Model Checking Circus -- Control Law Diagrams in Circus -- Security -- Verification of a Signature Architecture with HOL-Z -- End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform -- Formal Verification of Security Properties of Smart Card Embedded Source Code -- Networks and Processes -- A Formal Model of Addressing for Interoperating Networks -- An Approach to Unfolding Asynchronous Communication Protocols -- Semantics of BPEL4WS-Like Fault and Compensation Handling -- Abstraction, Retrenchment and Rewriting -- On Some Galois Connection Based Abstractions for the Mu-Calculus -- Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern -- Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion -- Scenarios and Modeling Languages -- Synthesis of Distributed Processes from Scenario-Based Specifications -- Verifying Scenario-Based Aspect Specifications -- An MDA Approach Towards Integrating Formal and Informal Modeling Languages -- Model Checking -- Model-Checking of Specifications Integrating Processes, Data and Time -- Automatic Symmetry Detection for Model Checking Using Computational Group Theory -- On Partitioning and Symbolic Model Checking -- Dynamic Component Substitutability Analysis -- Industry Day: Abstracts of Invited Talks -- Floating-Point Verification -- Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications -- Model-Based Testing in Practice -- Testing Concurrent Object-Oriented Systems with Spec Explorer -- ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software -- The Informal Nature of Systems Engineering. |
| Record Nr. | UNISA-996465825403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
FME '97 Industrial Applications and Strengthened Foundations of Formal Methods [[electronic resource] ] : 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997. Proceedings / / edited by John Fitzgerald, Cliff B. Jones, Peter Lucas
| FME '97 Industrial Applications and Strengthened Foundations of Formal Methods [[electronic resource] ] : 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997. Proceedings / / edited by John Fitzgerald, Cliff B. Jones, Peter Lucas |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XIV, 694 p.) |
| Disciplina | 005.1/01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Computer logic Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
| ISBN | 3-540-69593-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Diagrams and programming languages for programmable controllers -- Graphical specification and reasoning: Case study generalised railroad crossing -- A graphic notation for formal specifications of dynamic systems -- A semantic integration of object-Z and CSP for the specification of concurrent systems -- Class refinement and interface refinement in object-oriented programs -- Formalizing requirements for distributed systems with trace diagrams -- Consistent graphical specification of distributed systems -- Design of reactive control systems for event-driven operations -- An M-Net semantics for a real-time extension of µSDL -- Reconciling real-time with asynchronous message passing -- Specifying the remote controlling of valves in an explosion test environment -- PICGAL: Practical use of formal specification to develop a complex critical system -- Mathematical modeling and analysis of an external memory manager -- Automatic translation of VDM-SL specifications into gofer -- Towards an Integrated CASE and theorem proving tool for VDM-SL -- Specification of required non-determinism -- A corrected failure-divergence model for CSP in Isabelle/HOL -- A proof obligation generator for VDM-SL -- Verification of cryptographic protocols: An experiment -- TLA + PROMELA: Conjecture, check, proof -- A TLA solution to the specification and verification of the RLP1 retransmission protocol -- An efficient technique for deadlock analysis of large scale process networks -- Implementing a model checker for LEGO -- Formal verification of transformations for peephole optimization -- A meta-method for formal method integration -- Reuse of verified design templates through extended pattern matching -- A compositional proof system for shared variable concurrency -- A framework for modular formal specification and verification -- A timed semantics for the StateMate implementation of statecharts -- Using PVS to prove a Z refinement: A case study -- Verification of reactive systems using DisCo and PVS -- Term rewrite systems to derive set boolean operations on 2D objects -- A normal form reduction strategy for hardware/software partitioning -- Viewpoint consistency in Z and LOTOS: A case study -- A UNITY mapping operator for distributed programs. |
| Record Nr. | UNISA-996465506903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
FME '97 Industrial Applications and Strengthened Foundations of Formal Methods [[electronic resource] ] : 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997. Proceedings / / edited by John Fitzgerald, Cliff B. Jones, Peter Lucas
| FME '97 Industrial Applications and Strengthened Foundations of Formal Methods [[electronic resource] ] : 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997. Proceedings / / edited by John Fitzgerald, Cliff B. Jones, Peter Lucas |
| Edizione | [1st ed. 1997.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
| Descrizione fisica | 1 online resource (XIV, 694 p.) |
| Disciplina | 005.1/01/5113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Computer programming Programming languages (Electronic computers) Computer logic Software Engineering Programming Techniques Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
| ISBN | 3-540-69593-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Diagrams and programming languages for programmable controllers -- Graphical specification and reasoning: Case study generalised railroad crossing -- A graphic notation for formal specifications of dynamic systems -- A semantic integration of object-Z and CSP for the specification of concurrent systems -- Class refinement and interface refinement in object-oriented programs -- Formalizing requirements for distributed systems with trace diagrams -- Consistent graphical specification of distributed systems -- Design of reactive control systems for event-driven operations -- An M-Net semantics for a real-time extension of µSDL -- Reconciling real-time with asynchronous message passing -- Specifying the remote controlling of valves in an explosion test environment -- PICGAL: Practical use of formal specification to develop a complex critical system -- Mathematical modeling and analysis of an external memory manager -- Automatic translation of VDM-SL specifications into gofer -- Towards an Integrated CASE and theorem proving tool for VDM-SL -- Specification of required non-determinism -- A corrected failure-divergence model for CSP in Isabelle/HOL -- A proof obligation generator for VDM-SL -- Verification of cryptographic protocols: An experiment -- TLA + PROMELA: Conjecture, check, proof -- A TLA solution to the specification and verification of the RLP1 retransmission protocol -- An efficient technique for deadlock analysis of large scale process networks -- Implementing a model checker for LEGO -- Formal verification of transformations for peephole optimization -- A meta-method for formal method integration -- Reuse of verified design templates through extended pattern matching -- A compositional proof system for shared variable concurrency -- A framework for modular formal specification and verification -- A timed semantics for the StateMate implementation of statecharts -- Using PVS to prove a Z refinement: A case study -- Verification of reactive systems using DisCo and PVS -- Term rewrite systems to derive set boolean operations on 2D objects -- A normal form reduction strategy for hardware/software partitioning -- Viewpoint consistency in Z and LOTOS: A case study -- A UNITY mapping operator for distributed programs. |
| Record Nr. | UNINA-9910768453703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||