Brief description and aims of the program:

1. Modeling, analysis and verification of distributed networks. The use of highly distributed information, for example, in social networks, is demanding mechanisms to ensure the consistency and validity of data. Verification of the properties of the protocols is complex and therefore prototypes are needed to collect the formal protocol behavior. This group uses Maude for the modeling and proceeds to study the properties of the model.

2. Verification of workflow systems using Petri nets. We will study the decidability properties of various extensions of the basic Petri nets including names. The results obtained are applied to the study of the correction workflow networks with limited resources. In particular, we consider also quantitative aspects of these systems to assess the profitability that can be achieved by increasing our investment introducing new units of certain resources. We will also study the orchestration mechanisms, which are rules to coordinate in an efficient and secure way various tasks that take place in an independent manner within a system to take full advantage of the resources available, which obviously establish a limitation on system performance.

3. Coalgebraics semantics of process algebras. This technique is very useful in establishing systems and verifying properties of state (potentially) infinite. We are working on the study of different notions of simulation that may be of practical interest, studying the connections between them and the various categorical logic associated with them. The study of the semantics of processes is a highly technical subject, but offers the possibility of advancing in it if we can attract mathematicians of traditional court, which would find here a potential field of application.

4. Using Coq formalization of the semantics of parallel functional languages​​. We are studying parallel functional languages​​, in which intermingle the functional paradigm and parallelism feature. We have to describe with absolute precision the meanings of the various components that make one of those languages​​. These semantic descriptions are complex and it is interesting to have models performed by means of an automatic demonstrator, such as Coq. This establishes a new bridge between conventional mathematics and computer science, so this work will have a high component of interdisciplinarity.

5. Approximate testing. The correctness of a system with respect to a specification is dichotomous: either it is correct or incorrect. However, in practice the conditions set forth in the quality control tests are not so demanding in relation to the totality of desired properties of the system and certain deviations from desired ideal behavior are allowed. The development of this approach requires reasonable notions of distance between processes, which will be linked to the corresponding notions of semantics to establish the degree of strict correction cited above. We will need first to know all its properties, noting that they make them interesting on its application. Such application under the paradigm of testing force us back to start by defining in what sense a process passes a test with a given accuracy. To implement the testing framework developed approximate need ways of doing step test, supplemented by relevant theoretical studies that tell us how far we can get in the field to decide about properties of this framework.

 

Website:

http://www.ams.org/mathscinet/search/publications.html?pg1=IID&s1=271313

http://www.ams.org/mathscinet/search/publications.html?pg1=IID&s1=310074