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 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods for Components and Objects [[electronic resource] ] : 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers / / edited by Frank S. de Boer, Marcello M. Bonsangue, Stefan Hallerstede, Michael Leuschel |
Edizione | [1st ed. 2010.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 |
Descrizione fisica | 1 online resource (X, 339 p. 111 illus., 55 illus. in color.) |
Disciplina | 004.01/51 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Operating systems (Computers) Computer logic Computer programming Software Engineering Programming Languages, Compilers, Interpreters Operating Systems Logics and Meanings of Programs Software Engineering/Programming and Operating Systems Programming Techniques |
ISBN |
1-283-47734-3
9786613477347 3-642-17071-4 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996465963803316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Integrated Formal Methods [[electronic resource] ] : 7th International Conference, IFM 2009, Düsseldorf, Germany, February 16-19, 2009, Proceedings / / edited by Michael Leuschel, Heike Wehrheim |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
Descrizione fisica | 1 online resource (X, 367 p.) |
Disciplina | 005.1015113 |
Collana | Programming and Software Engineering |
Soggetto topico |
Computer logic
Software engineering Programming languages (Electronic computers) Computer programming Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques |
ISBN | 3-642-00255-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Developing Topology Discovery in Event-B -- Decomposition Structures for Event-B -- Taming the Unbounded for Hardware Synthesis -- Contributed Papers -- Verifying UML/OCL Operation Contracts -- Property Specifications for Workflow Modelling -- Formal Verification Based on Guided Random Walks -- Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format -- Changing System Interfaces Consistently: A New Refinement Strategy for CSP||B -- CSP with Hierarchical State -- Predicate Abstraction in a Program Logic Calculus -- Mechanised Translation of Control Law Diagrams into Circus -- Realizability of Choreographies Using Process Algebra Encodings -- Modelling Divergence in Relational Concurrent Refinement -- SAL-Based Symbolic Scheduling in Time-Triggered Networks -- Incremental Reasoning for Multiple Inheritance -- Model Checking LTL Formulae in RAISE with FDR -- An Introduction to Grammar Convergence -- Application of Graph Transformation in Verification of Dynamic Systems -- Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays -- Challenges in the Specification of Full Contracts -- Partial Order Reduction for State/Event LTL -- Dynamic Path Reduction for Software Model Checking -- Automatic Generation of Error Messages for the Symbolic Execution of EB3 Process Expressions -- Decompositional Petri Net Reductions. |
Record Nr. | UNISA-996465908603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Rigorous State-Based Methods : 10th International Conference, ABZ 2024, Bergamo, Italy, June 25–28, 2024, Proceedings / / edited by Silvia Bonfanti, Angelo Gargantini, Michael Leuschel, Elvinia Riccobene, Patrizia Scandurra |
Autore | Bonfanti Silvia |
Edizione | [1st ed. 2024.] |
Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 |
Descrizione fisica | 1 online resource (404 pages) |
Disciplina | 005.131 |
Altri autori (Persone) |
GargantiniAngelo
LeuschelMichael RiccobeneElvinia ScandurraPatrizia |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Machine theory
Computer engineering Computer networks Application software Logic programming Compilers (Computer programs) Formal Languages and Automata Theory Computer Engineering and Networks Computer and Information Systems Applications Logic in AI Compilers and Interpreters |
ISBN | 3-031-63790-9 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | 1 Invited Talk -- Formal Methods and Tools Applied in the Railway Domain -- 2 Research Papers -- Formal Modeling and Analysis of Apache Kafka in Alloy 6 -- Event-B Development of Modelling Human Intervention Request in Self- Driving Vehicle Systems -- Alloy Goes Fuzzy -- Transpilation of Petri-nets into B: Shallow and Deep Embeddings -- A Lean Reflective Abstract State Machine Definition -- Loose Observation in Event-B -- Modal Extensions of the Logic of Abstract State Machines -- An Analysis of the Impact of Field-Value Instance Navigation in Alloy’s Model Finding -- From Concept to Code: Unveiling a Tool for Translating Abstract State Machines into Java Code -- 3 Short Research Papers -- An Event-B Formal Model for Access Control and Resource Management of Serverless Apps -- Property Ownership Formal Modelling Using Event-B and iUML-B -- A Modeling and Verification Framework for Ethereum Smart Contracts -- Semantics Formalisation – From Event-B Contexts to Theories -- Using Symbolic Execution to Transform Turbo Abstract State Machines into Basic Abstract State Machines -- Multi-model Animation with Jeb -- Meta-Programming Event-B: Advancing Tool Support and Language Extensions -- Event-B as DSL in Isabelle and HOL -- ThoR: An Alloy5-based DSL for Interactive Theorem Proving in Coq -- Verifying HyperLTL properties in Event-B -- Small Step Incremental Verification of Compilers -- Designing Exception Handling using Event-B -- 4 Case Study -- The Mechanical Lung Ventilator Case Study -- Real-Time CCSL: Application to the Mechanical Lung Ventilator -- An Event-B Model of a Mechanical Lung Ventilator -- Modelling the Mechanical Lung Ventilation System using TASTD -- Modelling and Analysing a Mechanical Lung Ventilator in mCRL2 -- FRETting and Formal Modelling: A Mechanical Lung Ventilator -- 5 Doctoral Symposium -- From Event-B to Lambdapi -- Proof Construction and Checking on Evolving Abstract State Machines . |
Record Nr. | UNINA-9910866586803321 |
Bonfanti Silvia
![]() |
||
Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2024 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|