-
Learning How To Robustly Estimate Camera Pose in Endoscopic Videos
Authors:
Michel Hayoz,
Christopher Hahne,
Mathias Gallardo,
Daniel Candinas,
Thomas Kurmann,
Maximilian Allan,
Raphael Sznitman
Abstract:
Purpose: Surgical scene understanding plays a critical role in the technology stack of tomorrow's intervention-assisting systems in endoscopic surgeries. For this, tracking the endoscope pose is a key component, but remains challenging due to illumination conditions, deforming tissues and the breathing motion of organs. Method: We propose a solution for stereo endoscopes that estimates depth and o…
▽ More
Purpose: Surgical scene understanding plays a critical role in the technology stack of tomorrow's intervention-assisting systems in endoscopic surgeries. For this, tracking the endoscope pose is a key component, but remains challenging due to illumination conditions, deforming tissues and the breathing motion of organs. Method: We propose a solution for stereo endoscopes that estimates depth and optical flow to minimize two geometric losses for camera pose estimation. Most importantly, we introduce two learned adaptive per-pixel weight mappings that balance contributions according to the input image content. To do so, we train a Deep Declarative Network to take advantage of the expressiveness of deep-learning and the robustness of a novel geometric-based optimization approach. We validate our approach on the publicly available SCARED dataset and introduce a new in-vivo dataset, StereoMIS, which includes a wider spectrum of typically observed surgical settings. Results: Our method outperforms state-of-the-art methods on average and more importantly, in difficult scenarios where tissue deformations and breathing motion are visible. We observed that our proposed weight mappings attenuate the contribution of pixels on ambiguous regions of the images, such as deforming tissues. Conclusion: We demonstrate the effectiveness of our solution to robustly estimate the camera pose in challenging endoscopic surgical scenes. Our contributions can be used to improve related tasks like simultaneous localization and mapping (SLAM) or 3D reconstruction, therefore advancing surgical scene understanding in minimally-invasive surgery.
△ Less
Submitted 17 April, 2023;
originally announced April 2023.
-
A denotational semantics for PROMELA addressing arbitrary jumps
Authors:
Marco Comini,
María del Mar Gallardo,
Alicia Villanueva
Abstract:
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create…
▽ More
PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes.
In this paper, we introduce a bottom-up, fixpoint semantics that aims to model the behavior of PROMELA programs. This work is the first step towards a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.
△ Less
Submitted 27 August, 2021;
originally announced August 2021.
-
CataNet: Predicting remaining cataract surgery duration
Authors:
Andrés Marafioti,
Michel Hayoz,
Mathias Gallardo,
Pablo Márquez Neila,
Sebastian Wolf,
Martin Zinkernagel,
Raphael Sznitman
Abstract:
Cataract surgery is a sight saving surgery that is performed over 10 million times each year around the world. With such a large demand, the ability to organize surgical wards and operating rooms efficiently is critical to delivery this therapy in routine clinical care. In this context, estimating the remaining surgical duration (RSD) during procedures is one way to help streamline patient through…
▽ More
Cataract surgery is a sight saving surgery that is performed over 10 million times each year around the world. With such a large demand, the ability to organize surgical wards and operating rooms efficiently is critical to delivery this therapy in routine clinical care. In this context, estimating the remaining surgical duration (RSD) during procedures is one way to help streamline patient throughput and workflows. To this end, we propose CataNet, a method for cataract surgeries that predicts in real time the RSD jointly with two influential elements: the surgeon's experience, and the current phase of the surgery. We compare CataNet to state-of-the-art RSD estimation methods, showing that it outperforms them even when phase and experience are not considered. We investigate this improvement and show that a significant contributor is the way we integrate the elapsed time into CataNet's feature extractor.
△ Less
Submitted 21 June, 2021;
originally announced June 2021.
-
A Simulation Tool for tccp Programs
Authors:
María-del-Mar Gallardo,
Leticia Lavado,
Laura Panizo
Abstract:
The Timed Concurrent Constraint Language tccp is a declarative synchronous concurrent language, particularly suitable for modelling reactive systems. In tccp, agents communicate and synchronise through a global constraint store. It supports a notion of discrete time that allows all non-blocked agents to proceed with their execution simultaneously.
In this paper, we present a modular architecture…
▽ More
The Timed Concurrent Constraint Language tccp is a declarative synchronous concurrent language, particularly suitable for modelling reactive systems. In tccp, agents communicate and synchronise through a global constraint store. It supports a notion of discrete time that allows all non-blocked agents to proceed with their execution simultaneously.
In this paper, we present a modular architecture for the simulation of tccp programs. The tool comprises three main components. First, a set of basic abstract instructions able to model the tccp agent behaviour, the memory model needed to manage the active agents and the state of the store during the execution. Second, the agent interpreter that executes the instructions of the current agent iteratively and calculates the new agents to be executed at the next time instant. Finally, the constraint solver components which are the modules that deal with constraints.
In this paper, we describe the implementation of these components and present an example of a real system modelled in tccp.
△ Less
Submitted 3 January, 2017;
originally announced January 2017.
-
Using Model Checking to Generate Test Cases for Android Applications
Authors:
Ana Rosario Espada,
María del Mar Gallardo,
Alberto Salmerón,
Pedro Merino
Abstract:
The behavior of mobile devices is highly non deterministic and barely predictable due to the interaction of the user with its applications. In consequence, analyzing the correctness of applications running on a smartphone involves dealing with the complexity of its environment. In this paper, we propose the use of model-based testing to describe the potential behaviors of users interacting with mo…
▽ More
The behavior of mobile devices is highly non deterministic and barely predictable due to the interaction of the user with its applications. In consequence, analyzing the correctness of applications running on a smartphone involves dealing with the complexity of its environment. In this paper, we propose the use of model-based testing to describe the potential behaviors of users interacting with mobile applications. These behaviors are modeled by composing specially-designed state machines. These composed state machines can be exhaustively explored using a model checking tool to automatically generate all possible user interactions. Each generated trace model checker can be interpreted as a test case to drive a runtime analysis of actual applications. We have implemented a tool that follows the proposed methodology to analyze Android devices using the model checker Spin as the exhaustive generator of test cases.
△ Less
Submitted 9 April, 2015;
originally announced April 2015.
-
Modeling Hybrid Systems in the Concurrent Constraint Paradigm
Authors:
Damián Adalid,
María del Mar Gallardo,
Laura Titolo
Abstract:
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contra…
▽ More
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contrast to the variable/value style typical of imperative languages. Several extensions of ccp have been proposed in order to model reactive systems. One of these extensions is the Timed Concurrent Constraint Language (tccp) that adds to ccp a notion of discrete time and new features to model time-out and preemption actions. The goal of this paper is to explore the expressive power of tccp to describe hybrid systems. We introduce the language Hy-tccp as a conservative extension of tccp, by adding a notion of continuous time and new constructs to describe the continuous dynamics of hybrid systems. In this paper, we present the syntax and the operational semantics of Hy-tccp together with some examples that show the expressive power of our new language.
△ Less
Submitted 8 January, 2015;
originally announced January 2015.
-
Modeling Hybrid Systems in Hy-tccp
Authors:
Damian Adalid,
Maria del Mar Gallardo,
Laura Titolo
Abstract:
Concurrent,reactive and hybrid systems require quality modeling languages to be described and analyzed. The Timed Concurrent Constraint Language (tccp) was introduced as a simple but powerful model for reactive systems. In this paper, we present hybrid tccp (hy-tccp), an extension of tccp over continuous time which includes new con- structs to model the continuous dynamics of hybrid systems.
Concurrent,reactive and hybrid systems require quality modeling languages to be described and analyzed. The Timed Concurrent Constraint Language (tccp) was introduced as a simple but powerful model for reactive systems. In this paper, we present hybrid tccp (hy-tccp), an extension of tccp over continuous time which includes new con- structs to model the continuous dynamics of hybrid systems.
△ Less
Submitted 15 December, 2014;
originally announced December 2014.
-
Static Analysis using Parameterised Boolean Equation Systems
Authors:
María Del Mar Gallardo,
Christophe Joubert,
Pedro Merino
Abstract:
The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due to the presence of complex data structures. One recent and promising approach to deal with this problem is the construction of an abstract and correct representation of the global program state allowing to match visited states during program mo…
▽ More
The well-known problem of state space explosion in model checking is even more critical when applying this technique to programming languages, mainly due to the presence of complex data structures. One recent and promising approach to deal with this problem is the construction of an abstract and correct representation of the global program state allowing to match visited states during program model exploration. In particular, one powerful method to implement abstract matching is to fill the state vector with a minimal amount of relevant variables for each program point. In this paper, we combine the on-the-fly model-checking approach (incremental construction of the program state space) and the static analysis method called influence analysis (extraction of significant variables for each program point) in order to automatically construct an abstract matching function. Firstly, we describe the problem as an alternation-free value-based mu-calculus formula, whose validity can be checked on the program model expressed as a labeled transition system (LTS). Secondly, we translate the analysis into the local resolution of a parameterised boolean equation system (PBES), whose representation enables a more efficient construction of the resulting abstract matching function. Finally, we show how our proposal may be elegantly integrated into CADP, a generic framework for both the design and analysis of distributed systems and the development of verification tools.
△ Less
Submitted 3 July, 2006; v1 submitted 21 June, 2006;
originally announced June 2006.
