2 Search Results for "Doan, Ha Thi Thu"


Document
Short Paper
Towards Contract Modules for the Tezos Blockchain (Short Paper)

Authors: Thi Thu Ha Doan and Peter Thiemann

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)


Abstract
Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees. Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.

Cite as

Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{doan_et_al:OASIcs.FMBC.2021.5,
  author =	{Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{Towards Contract Modules for the Tezos Blockchain}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{5:1--5:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.5},
  URN =		{urn:nbn:de:0030-drops-154294},
  doi =		{10.4230/OASIcs.FMBC.2021.5},
  annote =	{Keywords: contract API, modules, static checking}
}
Document
Model Checking of Robot Gathering

Authors: Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata

Published in: LIPIcs, Volume 95, 21st International Conference on Principles of Distributed Systems (OPODIS 2017)


Abstract
Recent advances in distributed computing highlight models and algorithms for autonomous mo- bile robots that self-organize and cooperate together in order to solve a global objective. As results, a large number of algorithms have been proposed. These algorithms are given together with proofs to assess their correctness. However, those proofs are informal, which are error prone. This paper presents our study on formal verification of mobile robot algorithms. We first propose a formal model for mobile robot algorithms on anonymous ring shape network under multiplicity and asynchrony assumptions. We specify this formal model in Maude, a specification and pro- gramming language based on rewriting logic. We then use its model checker to formally verify an algorithm for robot gathering problem on ring enjoys some desired properties. As the result of the model checking, counterexamples have been found. We detect the sources of some unforeseen design errors. We, furthermore, give our interpretations of these errors.

Cite as

Ha Thi Thu Doan, François Bonnet, and Kazuhiro Ogata. Model Checking of Robot Gathering. In 21st International Conference on Principles of Distributed Systems (OPODIS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 95, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{doan_et_al:LIPIcs.OPODIS.2017.12,
  author =	{Doan, Ha Thi Thu and Bonnet, Fran\c{c}ois and Ogata, Kazuhiro},
  title =	{{Model Checking of Robot Gathering}},
  booktitle =	{21st International Conference on Principles of Distributed Systems (OPODIS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-061-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{95},
  editor =	{Aspnes, James and Bessani, Alysson and Felber, Pascal and Leit\~{a}o, Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2017.12},
  URN =		{urn:nbn:de:0030-drops-86324},
  doi =		{10.4230/LIPIcs.OPODIS.2017.12},
  annote =	{Keywords: Mobile Robot, Robot Gathering, Formal Verification, Model Checking, Maude}
}
  • Refine by Author
  • 1 Bonnet, François
  • 1 Doan, Ha Thi Thu
  • 1 Doan, Thi Thu Ha
  • 1 Ogata, Kazuhiro
  • 1 Thiemann, Peter

  • Refine by Classification
  • 1 Software and its engineering → Specification languages

  • Refine by Keyword
  • 1 Formal Verification
  • 1 Maude
  • 1 Mobile Robot
  • 1 Model Checking
  • 1 Robot Gathering
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2018
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail