LEADER 08171nam 22008175 450 001 996465312903316 005 20230330015535.0 010 $a3-642-30885-6 024 7 $a10.1007/978-3-642-30885-7 035 $a(CKB)3400000000085316 035 $a(SSID)ssj0000697433 035 $a(PQKBManifestationID)11426621 035 $a(PQKBTitleCode)TC0000697433 035 $a(PQKBWorkID)10691409 035 $a(PQKB)11386547 035 $a(PQKBManifestationID)16469621 035 $a(OCoLC)919164705 035 $a(PQKB)21323886 035 $a(DE-He213)978-3-642-30885-7 035 $a(MiAaPQ)EBC3070171 035 $a(PPN)168317958 035 $a(EXLCZ)993400000000085316 100 $a20120626d2012 u| 0 101 0 $aeng 135 $aurnn#008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aAbstract State Machines, Alloy, B, VDM, and Z$b[electronic resource] $eThird International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings /$fedited by John Derrick, John Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves, Elvinia Riccobene 205 $a1st ed. 2012. 210 1$aBerlin, Heidelberg :$cSpringer Berlin Heidelberg :$cImprint: Springer,$d2012. 215 $a1 online resource (XV, 378 p. 133 illus.) 225 1 $aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7316 300 $aInternational conference proceedings. 311 $a3-642-30884-8 320 $aIncludes bibliographical references and author index. 327 $tContribution to a Rigorous Analysis of Web Application Frameworks /$rEgon Bo?rger, Antonio Cisternino and Vincenzo Gervasi --$tIntegrated Operational Semantics: Small-Step, Big-Step and Multi-step /$rIan J. Hayes and Robert J. Colvin --$tTest Generation for Sequential Nets of Abstract State Machines /$rPaolo Arcaini, Francesco Bolis and Angelo Gargantini --$tASM and Controller Synthesis /$rRichard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu --$tContinuous ASM, and a Pacemaker Sensing Fragment /$rRichard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu --$tAn ASM Model of Concurrency in a Web Browser /$rVincenzo Gervasi --$tModeling the Supervisory Control Theory with Alloy /$rBenoi?t Fraikin, Marc Frappier and Richard St-Denis --$tPreventing Arithmetic Overflows in Alloy /$rAleksandar Milicevic and Daniel Jackson --$tExtending Alloy with Partial Instances /$rVajih Montaghami and Derek Rayside --$tToward a More Complete Alloy /$rTimothy Nelson, Daniel J. Dougherty, Kathi Fisler and Shriram Krishnamurthi --$tTemporal Logic Model Checking in Alloy /$rAmirhossein Vakili and Nancy A. Day --$tActive Attacking Multicast Key Management Protocol Using Alloy /$rTing Wang and Dongyao Ji --$tFormalizing Hybrid Systems with Event-B /$rJean-Raymond Abrial, Wen Su and Huibiao Zhu --$tSMT Solvers for Rodin /$rDavid De?harbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin --$tRefinement Plans for Informed Formal Design /$rGudmund Grov, Andrew Ireland and Maria Teresa Llano --$tRefinement by Interface Instantiation /$rStefan Hallerstede and Thai Son Hoang --$tDischarging Proof Obligations from Atelier B Using Multiple Automated Provers /$rDavid Mentre?, Claude Marche?, Jean-Christophe Fillia?tre and Masashi Asuka --$tA Semantic Analysis of Logics That Cope with Partial Terms /$rCliff B. Jones, Matthew J. Lovert and L. Jason Steggles --$tCombining VDM with Executable Code /$rClaus Ballegaard Nielsen, Kenneth Lausdahl and Peter Gorm Larsen --$tExtending the Test Template Framework to Deal with Axiomatic Descriptions, Quantifiers and Set Comprehensions /$rMaximiliano Cristia? and Claudia Frydman --$tA Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams /$rChris Marriott, Frank Zeyda and Ana Cavalcanti --$tVerification of Hardware Interaction Properties of Software /$rRamsay Taylor --$tUsing the Arbitrator Pattern for Dynamic Process-Instance Extension in a Work-Flow Management System /$rMatthes Elstermann, Detlef Seese and Albert Fleischmann --$tA Unified Processor Model for Compiler Verification and Simulation Using ASM /$rRoland Lezuo and Andreas Krall --$tModeling Synchronization/Communication Patterns in Vision-Based Robot Control Applications Using ASMs /$rAndrea Luzzana, Mattia Rossetti, Paolo Righettini and Patrizia Scandurra --$tA Reliability Prediction Method for Abstract State Machines /$rRaffaela Mirandola, Pasqualina Potena and Patrizia Scandurra --$tA Simplified Parallel ASM Thesis /$rKlaus-Dieter Schewe and Qing Wang --$tRefactoring Abstract State Machine Models /$rHamed Yaghoubi Shahir, Roozbeh Farahbod and Uwe Gla?sser --$tContinuous Behaviour in Event-B: A Sketch /$rRichard Banach, Huibiao Zhu, Wen Su and Xiaofeng Wu --$tFormal Verification of PLC Programs Using the B Method /$rHaniel Barbosa and David De?harbe --$tA Practical Event-B Refinement Method Based on a UML-Driven Development Process /$rThiago C. de Sousa, Paulo Se?rgio Muniz Silva and Colin F. Snook --$tLearn and Test for Event-B -- A Rodin Plugin /$rIonut Dinca, Florentin Ipate, Laurentiu Mierla and Alin Stefanescu --$tEvent-B Code Generation: Type Extension with Theories /$rAndrew Edmunds, Michael Butler, Issam Maamria, Renato Silva and Chris Lovell --$tFormal Proofs for the NYCT Line 7 (Flushing) Modernization Project /$rDenis Sabatier, Lilian Burdy, Antoine Requet and Je?ro?me Gue?ry --$tA Pattern for Modelling Fault Tolerant Systems in Event-B /$rGintautas Sulskus and Michael Poppleton. 330 $aThis book constitutes the proceedings of the Third International Conference on Abstract State Machines, B, VDM, and Z, which took place in Pisa, Italy, in June 2012. The 20 full papers presented together with 2 invited talks and 13 short papers were carefully reviewed and selected from 59 submissions. The ABZ conference series is dedicated to the cross-fertilization of five related state-based and machine-based formal methods: Abstract State Machines (ASM), Alloy, B, VDM, and Z. They share a common conceptual foundation and are widely used in both academia and industry for the design and analysis of hardware and software systems. The main goal of this conference series is to contribute to the integration of these formal methods, clarifying their commonalities and differences to better understand how to combine different approaches for accomplishing the various tasks in modeling, experimental validation and mathematical verification of reliable high-quality hardware/software systems. 410 0$aTheoretical Computer Science and General Issues,$x2512-2029 ;$v7316 606 $aComputer science 606 $aAlgorithms 606 $aComputer science?Mathematics 606 $aDiscrete mathematics 606 $aComputer Science Logic and Foundations of Programming 606 $aAlgorithms 606 $aTheory of Computation 606 $aMathematics of Computing 606 $aDiscrete Mathematics in Computer Science 615 0$aComputer science. 615 0$aAlgorithms. 615 0$aComputer science?Mathematics. 615 0$aDiscrete mathematics. 615 14$aComputer Science Logic and Foundations of Programming. 615 24$aAlgorithms. 615 24$aTheory of Computation. 615 24$aMathematics of Computing. 615 24$aDiscrete Mathematics in Computer Science. 676 $a006.3/1 686 $a54.53$2bcl 702 $aDerrick$b John$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aFitzgerald$b John$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aGnesi$b Stefania$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aKhurshid$b Sarfraz$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aLeuschel$b Michael$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aReeves$b Steve$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aRiccobene$b Elvinia$4edt$4http://id.loc.gov/vocabulary/relators/edt 712 12$aABZ (Conference) 906 $aBOOK 912 $a996465312903316 996 $aAbstract State Machines, Alloy, B, VDM, and Z$92829920 997 $aUNISA