We propose a presentation of Data-Aware Finite State Machines (DAFSM), a novel orchestration model for distributed systems. Inspired by the execution principles of Blockchain Smart Contracts, our model is suited for the specification and verification of multiparty distributed systems expressed with some annotated finite-state machines (FSMs). Our FSMs specify how the participants of a distributed protocol coordinate with each other. More precisely, the protocol is specified by an FSM capturing the expected control flow and global state of variables that participants share. In fact, we decorate transitions of FSMs with guards and assignments over data variables, and with participants binders. The latter allows to model scenarios with an unbounded number of participants which can vary at run-time.

Associate Professor at the Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon, Portugal (since October 2018). Founding member and Integrated researcher at the NOVA Laboratory for Computer Science and Informatics (NOVA LINCS), Portugal (since 2013). Assistant Professor at the Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon, Portugal ()2009 to 2018). Assistant Professor at the Section of Logic and Computation of the Department of Mathematics of IST. Technical University of Lisbon, Portugal (2000 to 2009).

PhD in Mathematics at IST, of the Technical University of Lisbon, Portugal (December 2000). MSc in Applied Mathematics at IST of the Technical University of Lisbon, Portugal (May 1996). BSc in Geographical Engineering at the Faculty of Sciences of the University of Lisbon, Portugal (September 1991).

Main research problem is how to ensure that inherently concurrent, highly distributed, software systems behave correctly. The focus is on the development of techniques, program constructions, and tools that help creating safe and well-behaved systems, provably providing correctness guarantees. The toolbox used includes static analysis of source code, capturing defects before deployment, with decidable, low complexity, property-driven, proof systems, using behavioural descriptions of programs.