Systems Engineering, Control and Robotics
The presentation will show the work that our group is developing in the areas of control, robotics
and vision and the projects where this works are being made. We work on the control, cooperation
and coordination of unmanned surface vessel (USVs) and unmanned aerial vehicles (UAVs) to get a
fast response in case of contingencies in the sea. We also work on stereo vision system for
autonomous landing of UAVs, controlling approaching maneuvers of USVs and also in application
of vision in agriculture.
Process Semantics and Models for Concurrency
Formal models of concurrency allows the precise and simple specification
of the behaviour and properties of that class of systems. Once non-determinism
appears as an unavoidable characteristic, the number of possibilities to develop
an adequate framework to formalize concurrent systems is enormous. At the
syntactic level process algebras are for sure the most simple and more used
framework, while Petri Nets are the favorite model when one looks for
graphical representations were the spatial distibution of evolving components
and the connections between them are expressed in a natural way.
In the case of process algebras operational semantics can be defined in a
quite simple way, but we need to develop other semantics in order to
abstract away from syntactic details that the operational semantics cannot
elliminate. It is quite surprising the big number of different semantics that we
can define to achieve that task, and this is not just a theoretical exercise, since
depending on the properties that one desire to take into account in his
developments each of the semantics could be the most adequate to use.
Moreover, we have also several ways to define these semantics and is
important to have a rich metatheory that relates all of them in a simple way.
Advanced Network Technologies:
Next Generation Mobile Networks,
As an interdisciplinary research team of the UCM, GASS integrates mathematical solutions
into different environments and applies them to a broad range of problems. The research
concentrates on the design, evaluation and implementation of cryptographic algorithms and
protocols, and on the development of security architectures for information and communication
systems. The applications areas are privacy, identity management and anonymous communications,
as well as trusted platforms. A relatively new research topic deals with mobile ad hoc
networks (MANETs), wireless sensors networks (WSNs) and next generation mobile networks.
GASS evaluates and develops security for wireless and mobile networks.
Mobile Ad Hoc Networks,
Wireless Sensor Networks and Computer Security
Infinite State Systems
In this talk I will present the work done by our group in the past few years in the area of
verification of infinite state systems. A well known formalism for the specification
of infinite state systems is Petri Nets. Petri Nets enjoy several nice properties which
make them "easy to analyse", in the sense of having many decidability results for their
verification. We have been working on the study of extensions of Petri nets for mobility
and security. In that line, I will define nu-Petri nets, a model of Petri nets extended with dynamic
fresh name creation and name management, and I will comment on the known decidability and
complexity results for them. Finally, I will discuss some ongoing work.