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,
Mobile Ad Hoc Networks, Wireless Sensor Networks and Computer Security

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.

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.