Search results for "TLA"

Hits ?▲	Authors	Title	Venue	Year	Link
21	Jure Kukovec, Thanh-Hai Tran 0002, Igor Konnov 0001	Extracting symbolic transitions from TLA+ specifications.	Sci. Comput. Program.	2020	DBLP DOI BibTeX RDF
21	Gefei Zhang	Specifying and Model Checking Workflows of Single Page Applications with TLA+.	QRS Companion	2020	DBLP DOI BibTeX RDF
21	Nawar H. Obeidat, Carla Purdy	Modeling a Smart School Building System Using UML and TLA+.	ICICT	2020	DBLP DOI BibTeX RDF
21	Giulio Salierno, Sabatino Morvillo, Letizia Leonardi, Giacomo Cabri	Specification and verification of railway safety-critical systems using TLA+: A Case Study.	WETICE	2020	DBLP DOI BibTeX RDF
21	Peter Zeller 0001, Annette Bieniusa, Carla Ferreira 0001	Teaching practical realistic verification of distributed algorithms in Erlang with TLA+.	Erlang Workshop	2020	DBLP DOI BibTeX RDF
21	Tim Soethout, Tijs van der Storm, Jurgen J. Vinju	Automated Validation of State-Based Client-Centric Isolation with TLA+.	SEFM	2020	DBLP DOI BibTeX RDF
21	Igor Konnov 0001, Jure Kukovec, Thanh-Hai Tran 0002	TLA+ model checking made symbolic.	Proc. ACM Program. Lang.	2019	DBLP DOI BibTeX RDF
21	Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts 0001	The TLA+ Toolbox.	F-IDE@FM	2019	DBLP DOI BibTeX RDF
21	Yu Gao, Hua Li, Yuanping Li, Bowei Liu, Xianrong Wang, Hongwei Ruan	Using TLA+ to Specify Leader Election of Raft Algorithm with Consideration of Leadership Transfer in Multiple Controllers.	QRS Companion	2019	DBLP DOI BibTeX RDF
21	Aurélie Hurault, Philippe Quéinnec	Proving a Non-blocking Algorithm for Process Renaming with TLA ^+ +.	TAP@FM	2019	DBLP DOI BibTeX RDF
21	Saba Latif, Aniqa Rehman, Nazir Ahmad Zafar	Blockchain and IoT Based Formal Model of Smart Waste Management System Using TLA+.	FIT	2019	DBLP DOI BibTeX RDF
21	Antonios Gouglidis, Christos Grompanopoulos, Anastasia Mavridou	Formal Verification of Usage Control Models: A Case Study of UseCON Using TLA+.	MeTRiD@ETAPS	2018	DBLP DOI BibTeX RDF
21	Stephan Merz, Hernán Vanzetto	Encoding TLA+ into unsorted and many-sorted first-order logic.	Sci. Comput. Program.	2018	DBLP DOI BibTeX RDF
21	Ali Abbassi, Amin Bandali, Nancy A. Day, José Serna	A Comparison of the Declarative Modelling Languages B, Dash, and TLA+.	MoDRE@RE	2018	DBLP DOI BibTeX RDF
21	Pedro Yuri Arbs Paiva, Osamu Saotome, Christof Brandauer	Specification and Verification of a Multi-agent Coordination Protocol with TLA+.	SBESC	2018	DBLP DOI BibTeX RDF
21	Michael J. Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl (eds.)	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings	ABZ	2018	DBLP DOI BibTeX RDF
21	Jean-Raymond Abrial	The ABZ-2018 Case Study with Event-B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Wen Su, Jinxin Chen, Shehroz Khan 0002	Insulin Pump: Modular Modeling of Hybrid Systems Using Event-B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Dana Dghaym, Michael Poppleton, Colin F. Snook	Diagram-Led Formal Modelling Using iUML-B for Hybrid ERTMS Level 3.	ABZ	2018	DBLP DOI BibTeX RDF
21	Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo, Jeanne Tawa	Proposition of an Action Layer for Electrum.	ABZ	2018	DBLP DOI BibTeX RDF
21	Yamine Aït Ameur, Idir Aït-Sadoune, P. Casteran, J. Paul Gibson, Kahina Hacid, Souad Kherroubi, Dominique Méry, Linda Mohand-Oussaïd, Neeraj Kumar Singh 0001, Laurent Voisin	On the Importance of Explicit Domain Modelling in Refinement-Based Modelling Design. Experiments with Event-B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Klaus-Dieter Schewe, Loredana Tec, Qing Wang 0002	Capturing Membrane Computing by ASMs.	ABZ	2018	DBLP DOI BibTeX RDF
21	Christoph Beierle, Klaus-Dieter Schewe	Abstract State Machines with Exact Real Arithmetic.	ABZ	2018	DBLP DOI BibTeX RDF
21	Flavio Ferrarotti, Senén González, Klaus-Dieter Schewe, José Maria Turull Torres	Systematic Refinement of Abstract State Machines with Higher-Order Logic.	ABZ	2018	DBLP DOI BibTeX RDF
21	Steve Jeffrey Tueno Fotso, Amel Mammar, Régine Laleau, Marc Frappier	Event-B Expression and Verification of Translation Rules Between SysML/KAOS Domain Models and B System Specifications.	ABZ	2018	DBLP DOI BibTeX RDF
21	Kaiyuan Wang, Allison Sullivan, Manos Koukoutos, Darko Marinov, Sarfraz Khurshid	Systematic Generation of Non-equivalent Expressions for Relational Algebra.	ABZ	2018	DBLP DOI BibTeX RDF
21	John W. Baugh Jr., Tristan Dyer	State-Based Formal Methods in Scientific Computation.	ABZ	2018	DBLP DOI BibTeX RDF
21	Philipp Paulweber, Emmanuel Pescosta, Uwe Zdun	CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation.	ABZ	2018	DBLP DOI BibTeX RDF
21	Markus Leitz, Alexander Raschke	Formal Specification of the Semantics of Control State Diagrams.	ABZ	2018	DBLP DOI BibTeX RDF
21	Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh, Asieh Salehi Fathabadi	Verifiable Code Generation from Scheduled Event-B Models.	ABZ	2018	DBLP DOI BibTeX RDF
21	Janet Barnes, Jonathan Hammond, Angela Wallenburg, Thomas Wilson	ABZ Languages and Tools in Industrial-Scale Application.	ABZ	2018	DBLP DOI BibTeX RDF
21	Farah Al-Shareefi, Alexei Lisitsa 0001, Clare Dixon	Clarification of Ambiguity for the Simple Authentication and Security Layer.	ABZ	2018	DBLP DOI BibTeX RDF
21	Paolo Arcaini, Pavel Jezek, Jan Kofron	Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin.	ABZ	2018	DBLP DOI BibTeX RDF
21	Dominik Hansen, Michael Leuschel, David Schneider 0001, Sebastian Krings, Philipp Körner, Thomas Naulin, Nader Nayeri, Frank Skowron	Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains.	ABZ	2018	DBLP DOI BibTeX RDF
21	Inna Vistbakka, Mikhail Barash, Elena Troubitsyna	Towards Creating a DSL Facilitating Modelling of Dynamic Access Control in Event-B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Frédéric Badeau, Vincent Lacroix, Vincent Monfort, Laurent Voisin, Christophe Métayer	Modelling Dynamic Data Structures with the B Method.	ABZ	2018	DBLP DOI BibTeX RDF
21	Alcino Cunha, Nuno Macedo	Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum.	ABZ	2018	DBLP DOI BibTeX RDF
21	Thai Son Hoang, Michael J. Butler, Klaus Reichl	The Hybrid ERTMS/ETCS Level 3 Case Study.	ABZ	2018	DBLP DOI BibTeX RDF
21	Silvia Bonfanti, Angelo Gargantini, Atif Mashkoor	AsmetaA: Animator for Abstract State Machines.	ABZ	2018	DBLP DOI BibTeX RDF
21	Klaus-Dieter Schewe, Flavio Ferrarotti, Loredana Tec, Qing Wang 0002	Distributed Adaptive Systems - Theory, Specification, Reasoning.	ABZ	2018	DBLP DOI BibTeX RDF
21	Guillaume Dupont, Yamine Aït Ameur, Marc Pantel, Neeraj Kumar Singh 0001	Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Richard Banach	Issues in Automated Urban Train Control: 'Tackling' the Rugby Club Problem.	ABZ	2018	DBLP DOI BibTeX RDF
21	Chenyang Zhu 0001, Michael J. Butler, Corina Cîrstea	Refinement of Timing Constraints for Concurrent Tasks with Scheduling.	ABZ	2018	DBLP DOI BibTeX RDF
21	Kaiyuan Wang, Allison Sullivan, Darko Marinov, Sarfraz Khurshid	Solver-Based Sketching of Alloy Models Using Test Valuations.	ABZ	2018	DBLP DOI BibTeX RDF
21	Amel Mammar, Marc Frappier, Steve Jeffrey Tueno Fotso, Régine Laleau	An Event-B Model of the Hybrid ERTMS/ETCS Level 3 Standard.	ABZ	2018	DBLP DOI BibTeX RDF
21	Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier, Michael Leuschel	A Translation from Alloy to B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Guillaume Bury, Simon Cruanes, David Delahaye, Pierre-Louis Euvrard	An Automation-Friendly Set Theory for the B Method.	ABZ	2018	DBLP DOI BibTeX RDF
21	Steve Jeffrey Tueno Fotso, Marc Frappier, Régine Laleau, Amel Mammar	Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach.	ABZ	2018	DBLP DOI BibTeX RDF
21	Lilian Burdy, David Déharbe	Teaching an Old Dog New Tricks - The Drudges of the Interactive Prover in Atelier B.	ABZ	2018	DBLP DOI BibTeX RDF
21	Jean-Raymond Abrial	On B and Event-B: Principles, Success and Challenges.	ABZ	2018	DBLP DOI BibTeX RDF
21	Leslie Lamport, Stephan Merz	Auxiliary Variables in TLA+.	CoRR	2017	DBLP BibTeX RDF
21	Stefan Resch, Michael Paulitsch	Using TLA+ in the Development of a Safety-Critical Fault-Tolerant Middleware.	ISSRE Workshops	2017	DBLP DOI BibTeX RDF
21	Nuno Macedo, Alcino Cunha	Alloy meets TLA+: An exploratory study.	CoRR	2016	DBLP BibTeX RDF
21	Dominik Hansen, Michael Leuschel	Translating B to TLA+ for validation with TLC.	Sci. Comput. Program.	2016	DBLP DOI BibTeX RDF
21	Philip Johnson-Freyd, Geoffrey C. Hulette, Zena M. Ariola	Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System.	FMICS-AVoCS	2016	DBLP DOI BibTeX RDF
21	Michael J. Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklós Biró (eds.)	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings	ABZ	2016	DBLP DOI BibTeX RDF
21	Yuhui Lin, Gudmund Grov, Colin O'Halloran, Priiya G.	A Super Industrial Application of PSGraph.	ABZ	2016	DBLP DOI BibTeX RDF
21	Flavio Ferrarotti, Loredana Tec, José Maria Turull Torres	Towards an ASM Thesis for Reflective Sequential Algorithms.	ABZ	2016	DBLP DOI BibTeX RDF
21	Atif Mashkoor	The Hemodialysis Machine Case Study.	ABZ	2016	DBLP DOI BibTeX RDF
21	Guillaume Babin, Yamine Aït Ameur, Neeraj Kumar Singh 0001, Marc Pantel	Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development.	ABZ	2016	DBLP DOI BibTeX RDF
21	John W. Baugh Jr., Alper Altuntas	Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy.	ABZ	2016	DBLP DOI BibTeX RDF
21	Gudmund Grov, Andrew Ireland, Maria Teresa Llano, Peter Kovacs, Simon Colton, Jeremy Gow	Semi-Automated Design Space Exploration for Formal Modelling.	ABZ	2016	DBLP DOI BibTeX RDF
21	Dominik Hansen, David Schneider 0001, Michael Leuschel	Using B and ProB for Data Validation Projects.	ABZ	2016	DBLP DOI BibTeX RDF
21	Yibo Liang, Yuhui Lin, Gudmund Grov	'The Tinker' for Rodin.	ABZ	2016	DBLP DOI BibTeX RDF
21	Egon Börger	Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets.	ABZ	2016	DBLP DOI BibTeX RDF
21	Felix Kossak, Atif Mashkoor	How to Select the Suitable Formal Method for an Industrial Application: A Survey.	ABZ	2016	DBLP DOI BibTeX RDF
21	Rajiv Murali, Andrew Ireland, Gudmund Grov	UC-B: Use Case Modelling with Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra, Michael Stegmaier	Unified Syntax for Abstract State Machines.	ABZ	2016	DBLP DOI BibTeX RDF
21	Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene	How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study.	ABZ	2016	DBLP DOI BibTeX RDF
21	Michael Leuschel, Egon Börger	A Compact Encoding of Sequential ASMs in Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Dana Dghaym, Matheus Garay Trindade, Michael J. Butler, Asieh Salehi Fathabadi	A Graphical Tool for Event Refinement Structures in Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Andrew Edmunds, Colin F. Snook, Marina Waldén	On Component-Based Reuse for Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz	Proving Determinacy of the PharOS Real-Time Operating System.	ABZ	2016	DBLP DOI BibTeX RDF
21	Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander B. Romanovsky	Rodin Platform Why3 Plug-In.	ABZ	2016	DBLP DOI BibTeX RDF
21	Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel	Generating Event-B Specifications from Algorithm Descriptions.	ABZ	2016	DBLP DOI BibTeX RDF
21	Artur Oliveira Gomes, Andrew Butterfield	Modelling the Haemodialysis Machine with Circus.	ABZ	2016	DBLP DOI BibTeX RDF
21	Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif	A Relational Encoding for a Clash-Free Subset of ASMs.	ABZ	2016	DBLP DOI BibTeX RDF
21	Michael Stegmaier, Marcel Dausend, Alexander Raschke, Matthias Tichy	A Universal Control Construct for Abstract State Machines.	ABZ	2016	DBLP DOI BibTeX RDF
21	Philipp Paulweber, Uwe Zdun	A Model-Based Transformation Approach to Reuse and Retarget CASM Specifications.	ABZ	2016	DBLP DOI BibTeX RDF
21	David Mentré	SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysML.	ABZ	2016	DBLP DOI BibTeX RDF
21	Noran Azmy, Stephan Merz, Christoph Weidenbach	A Rigorous Correctness Proof for Pastry.	ABZ	2016	DBLP DOI BibTeX RDF
21	Richard Banach	Hemodialysis Machine in Hybrid Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Sebastian Krings, Michael Leuschel	Proof Assisted Symbolic Model Checking for B and Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Ivaylo Dobrikov, Michael Leuschel	Enabling Analysis for Event-B.	ABZ	2016	DBLP DOI BibTeX RDF
21	Thomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau	Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods.	ABZ	2016	DBLP DOI BibTeX RDF
21	Thai Son Hoang, Colin F. Snook, Lukas Ladenberger, Michael J. Butler	Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation.	ABZ	2016	DBLP DOI BibTeX RDF
21	Joshua Schmidt, Sebastian Krings, Michael Leuschel	Interactive Model Repair by Synthesis.	ABZ	2016	DBLP DOI BibTeX RDF
21	Maha Boussabbeh, Mohamed Tounsi 0001, Mohamed Mosbah 0001, Ahmed Hadj Kacem	Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions.	ABZ	2016	DBLP DOI BibTeX RDF
21	Florent Chevrou, Aurélie Hurault, Philippe Quéinnec	Automated Verification of Asynchronous Communicating Systems with TLA+.	Electron. Commun. Eur. Assoc. Softw. Sci. Technol.	2015	DBLP DOI BibTeX RDF
21	Stephan Merz, Hernán Vanzetto	Encoding TLA+ set theory into many-sorted first-order logic.	CoRR	2015	DBLP BibTeX RDF
21	Amira Methni, Matthieu Lemerre, Belgacem Ben Hedia, Serge Haddad, Kamel Barkaoui	Specifying and Verifying Concurrent C Programs with TLA+.	FTSCS	2014	DBLP DOI BibTeX RDF
21	Zhen You, Jinyun Xue, Qimin Hu, Yi Hong 0005	Formal Semantics of Orc Based on TLA+.	SOFL+MSVL	2014	DBLP DOI BibTeX RDF
21	Frédéric Boniol, Virginie Wiels, Yamine Aït Ameur, Klaus-Dieter Schewe (eds.)	ABZ 2014: The Landing Gear Case Study - Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, Toulouse, France, June 2-6, 2014. Proceedings	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF
21	Yamine Aït Ameur, Klaus-Dieter Schewe (eds.)	Abstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings	ABZ	2014	DBLP DOI BibTeX RDF
21	Stephan Merz, Hernán Vanzetto	Refinement Types for tla +.	NASA Formal Methods	2014	DBLP DOI BibTeX RDF
21	Paolo Arcaini, Angelo Gargantini, Elvinia Riccobene	Offline Model-Based Testing and Runtime Monitoring of the Sensor Voting Module.	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF
21	Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto, Michael Leuschel	Validation of the ABZ Landing Gear System Using ProB.	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF
21	Richard Banach	The Landing Gear Case Study in Hybrid Event-B.	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF
21	Wen Su, Jean-Raymond Abrial	Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System.	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF
21	Amel Mammar, Régine Laleau	Modeling a Landing Gear System in Event-B.	ABZ (Case Study)	2014	DBLP DOI BibTeX RDF