Hugo A. López | publications

2020

BPM

Understanding Quality of Declarative Process Models Through the Mental Models of Experts Andaloussi, Amine Abbad, Davis, Christopher J., Burattin, Andrea, López, Hugo A., Slaats, Tijs, and Weber, Barbara In International Conference on Business Process Management (BPM) 2020 [Abstract] [Publisher's copy] [Preprint]
Imperative process models have become immensely popular.However, their use is usually limited to rigid and repetitive processes.Considering the inherent flexibility in most processes in the real-worldand the increased need for managing knowledge-intensive processes, theadoption of declarative languages becomes more pertinent than ever.While the quality of imperative models has been extensively investigatedin the literature, little is known about the dimensions affecting the qual-ity of declarative models. This work takes an advanced stride to investi-gate the quality of declarative models. Following the theory of PersonalConstruct Psychology (PCT), our research introduces a novel methodwithin the Business Process Management (BPM) field to explore qual-ity in the eyes of expert modelers. The findings of this work summarizethe dimensions defining the quality of declarative models. The outcomeshows the potential of PCT as a basis to discover quality dimensions andadvances our understanding of quality in declarative process models.
J. Int. Relations

Digital Experiences in Creating Digital Services: Case Work for the Rights of the Child López, Hugo A. Journal of the Belarusian State University. International Relations. 2020 [Abstract] [Publisher's copy]
The digitalization process in the public sector has brought different benefits to states and their citizens, but it has also brought several challenges. In particular, digitalization processes require close collaboration with legal practitioners, managers and IT professionals, and failure to engage all participants means to come up with digital systems that do not comply with requirements, especially those related to laws. Currently, compliance is done in an after-the-fact fashion: a digital system is implemented, and legislators audit whether it abides legal constraints. The problem with this approach is the cost: in case of non-compliance, systems need to be re-implemented, and this will be most likely the case since laws are always changing. In this work we report experiences in compliant-by-design case work (CbDCW). In CbDCW, legal considerations are involved before the system is implemented, making compliance checking a task that can be automated. Moreover, the impact of a law change in implementation can be identified without needing to program a new solution. This paper reports our experiences in the application of CbDCW in the Danish public sector, as well as to propose a research agenda derived from these experiences. Overall we identified that there are key socio-technical differences between legal practitioners and process or IT developers, and that ensuring compliance requires these types of stakeholders to have a common understanding, which can be supported by hybrid-modeling techniques proper from business process management.
ICSSP

EcoKnow: Engineering Effective, Co-created and Compliant Adaptive Case Management Systems for Knowledge Workers Hildebrandt, Thomas T., Andaloussi, Amine Abbad, Christensen, Lars R., Debois, Søren, Healy, Nicklas Pape, López, Hugo A., Marquard, Morten, Møller, Naja L. H., and Petersen, Anette C. M. In International Conference on Software and Systems Process (ICSSP) 2020 [Abstract] [Publisher's copy] [Preprint]
We report on a new approach to co-creating adaptive case manage- ment systems jointly with end-users, developed in the context of the Effective co-created and compliant adaptive case Management Systems for Knowledge Workers (EcoKnow.org) research project. The approach is based on knowledge from prior ethnographic field stud- ies and research in the declarative Dynamic Condition Response (DCR) technology for model-driven design of case management systems. The approach was tested in an operational environment jointly with the danish municipality of Syddjurs by conducting a service-design project and implementing an open source case manager tool and a new highlighter tool for mapping between tex- tual specifications and the DCR notation. The design method and technologies were evaluated by understandability studies with end- users. The study showed that the development could be done in just 6 months, and that the new highlighter tool in combination with the traditional design and simulation tools, supports domain experts formalise and provide traceability between their interpretations of textual specifications and the formal models.
FASE

Business Process Compliance using Reference Models of Law López, Hugo A., Debois, Søren, Slaats, Tijs, and Hildebrandt, Thomas T. In 23rd Intl. Conf. on Fundamental Approaches to Software Engineering (FASE) 2020 [Abstract] [Publisher's copy] [Preprint]
Legal compliance is an important part of certifying the correct behaviour of a business process. To be compliant, organizations might hard-wire regulations into processes, limiting the discretion that workers have when choosing what activities should be executed in a case. Worse, hard-wired compliant processes are difficult to change when laws change, and this occurs very often. This paper proposes a model-driven approach to process compliance and combines a) reference models from laws, and b) business process models. Both reference and process models are expressed in a declarative process language, The Dynamic Condition Response (DCR) graphs. They are subject to testing and verification, allowing law practitioners to check consistency against the intent of the law. Compliance checking is a combination of alignments between events in laws and events in a process model. In this way, a reference model can be used to check different process variants. Moreover, changes in the reference model due to law changes do not necessarily invalidate existing processes, allowing their reuse and adaptation. We exemplify the framework via the alignment of laws and business rules and a real contract change management process, Finally, we show how compliance checking for declarative processes is decidable, and provide a polynomial time approximation that contrasts NP complexity algorithms used in compliance checking for imperative business processes. All-together, this paper presents technical and methodological steps that are being used by legal practitioners in municipal governments in their efforts towards digitalization of work practices in the public sector
iFM

Chain of events: Modular Process Models for the Law Debois, Søren, López, Hugo A., Slaats, Tijs, Andaloussi, Amine Abbad, and Hildebrandt, Thomas T. In 16th International Conference on integrated Formal Methods (iFM) 2020 [Abstract] [Publisher's copy] [Preprint]
In this paper, we take technical and practical steps towards the modularisation of compliant-by-design executable declarative process models. First, we demonstrate by example how the specific language of timed DCR graphs is capable of modelling complex legislation, with ex- amples from laws regulating the functioning of local governments in Den- mark. We then identify examples of law paragraphs that are beyond these modelling capabilities. This incompatibility arises from subtle and—from a computer science perspective—non-standard interactions between dis- tinct paragraphs of the law, which must then become similar interactions between model fragments. To encompass these situations, we propose a notion of networks of processes, where the processes are allowed to in- teract and regulate their interaction through the novel mechanisms of exclusion and linking. Networks are parametric in the underlying process formalism, allowing interactions between processes specified in arbitrary and possibly distinct trace-language semantics formalisms as the indi- vidual models. Technically, we provide a sufficient condition for a good class of network compositions to realise refinement of the constituent processes. Finally, parts of the theoretical framework (networks and ex- clusion) have been implemented by our industry partners, and we report on a preliminary evaluation suggesting that inter-model synchronisation is indeed both necessary and helpful in practical modelling scenarios.
A Type Discipline for Message Passing Parallel Programs Vasconcelos, Vasco Thudichum, Martins, Francisco, López, Hugo A., and Yoshida, Nobuko 2020
Declarative interpretations of session-based concurrency Cano, Mauricio, López, Hugo A., Pérez, Jorge A., and Rueda, Camilo 2020

2019

EDOC

Assisted Declarative Process Creation from Natural Language Descriptions López, Hugo A., Marquard, Morten, Muttenhaler, Lukas, and Strømsted, Rasmus In 23rd IEEE International Enterprise Distributed Object Computing (EDOC) 2019 [Abstract] [Publisher's copy] [Preprint]
In this paper, we report recent advances on user support for declarative process generation from natural language descriptions. The Process Highlighter is a hybrid-modelling tool that facilitates the (manual) creation of Dynamic Response Condition (DCR) graphs directly from text documents, supporting non-technical users in the adoption of declarative process models. While some process descriptions are a few paragraphs long, others, such as the ones coming from municipal governments and legal bodies might contain several pages. Some aspects that undermine the adoption of hybrid modelling techniques and their promised one-to-one correspondence between texts and process models are the length of the texts, the inconsistent use of terms, and the difficulty in identifying textual elements that correspond to elements in a declarative process model. To mitigate these risks, we have implemented major additions in the Process Highlighter for industrial usage. The principal change is the inclusion of Natural Language Processing (NLP) techniques to support users in the identification of roles, activities and constraints. This, combined with the modelling, simulation and verification tools already existing in the framework, support the users in providing process models that are better aligned with their specifications, in a shorter time. These features are motivated from empirical observations of the use of the Process Highlighter in groups of caseworkers and students of process engineering in Danish universities.
FORTE

Declarative Choreographies and Liveness Hildebrandt, Thomas T., Slaats, Tijs, López, Hugo A., Debois, Søren, and Carbone, Marco In Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 [Abstract] [Publisher's copy] [Preprint]
We provide the first formal model for declarative choreographies, which is able to express general omega-regular liveness properties. We use the Dynamic Condition Response (DCR) graphs notation for both choreographies and end-points. We define end-point projection as a restriction of DCR graphs and derive the condition for end-point projectability from the causal relationships of the graph. We illustrate the results with a running example of a Buyer-Seller-Shipper protocol. All the examples are available for simulation in the online DCR workbench at http://dcr.tools/forte19.
ER

Exploring the Modeling of Declarative Processes Using a Hybrid Approach Andaloussi, Amine Abbad, Buch-Lorentsen, Jon, López, Hugo A., Slaats, Tijs, and Weber, Barbara In Conceptual Modeling (ER) 2019 [Abstract] [Publisher's copy] [Preprint]
Process modeling aims at providing an external representation of a business process in the shape of a process model. The complexity of the modeling language, the usability of the modeling tool, and the expertise of the modeler are among the key factors defining the difficulty of a modeling task. Following a qualitative analysis approach, this work explores a hybrid modeling technique enhanced with a tool (i.e., the Highlighter) to guide the transition from informal text-based process descriptions to formal declarative process models. The exploratory results suggest that this technique provides cognitive support to modelers and hint towards an enhanced quality of process models in terms of alignment, traceability of process requirements and availability of documentation. The outcome of this work shows a clear opportunity for future work and provides a framework for further empirical studies.
Towards Legally Compliant Governmental Case Work with Dynamic Condition Response Graphs López, Hugo A., Debois, Søren, and Hildebrandt, Thomas T. 2019

2018

Compliance-driven Process Development with DCR Graphs López, Hugo A. In EcoKnow’2018 - CAISE 2018 Workshops 2018
BPM

The Process Highlighter: From Texts to Declarative Processes and Back López, Hugo A., Debois, Søren, Hildebrandt, Thomas T., and Marquard, Morten In Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2018 co-located with 16th International Conference on Business Process Management (BPM 2018), Sydney, Australia, September 9-14, 2018. 2018 [Abstract] [Publisher's copy] [Preprint]
The adoption of formal models by process specialists has faced two challenges: First, it requires process specialists to get training in formal modeling. Second, the resulting specifications bear little resemblance wrt. the original descriptions. We introduce a tool that supports translations between natural language descriptions and declarative process models. The resulting models are given in a graphical formalism, DCR Graphs. Traceability is at the core of the tool: Later changes in the process model due to, eg, ambiguity resolution are traced back into the text. This allows users to either correct and complete their descriptions, or to derive models more refined than the text. In this paper, we describe the mechanics of the tool and provide examples of its use. Finally, we report on experiences using the tool in a Danish Municipal government.
BPM

Dynamic Evaluation Forms using Declarative Modeling Strømsted, Rasmus, López, Hugo A., Debois, Søren, and Marquard, Morten In Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2018 co-located with 16th International Conference on Business Process Management (BPM 2018), Sydney, Australia, September 9-14, 2018. 2018 [Abstract] [Publisher's copy] [Preprint]
This paper reports preliminary experiences using the Dynamic Condition Response (DCR) graphs declarative process notation to specify dynamic evaluation forms, and using an execution engine for that notation to subsequently “run” the form. The DCR notation was able to express all the patterns of behaviour necessary for a real case: a post-hoc evaluation form for a Danish arbitration court,“Voldgiftsnævnet for Anlæg og Byggeri”. However, some patterns were somewhat cumbersome to express.

2017

SAC

Choreographing cyber-physical distributed control systems for the energy sector López, Hugo A., and Heussen, Kai In ACM Simposium of Applied Computing, SAC 2017 [Abstract] [Publisher's copy] [Preprint]
Energy Systems are facing a significant change in the way their management and control is conceived. With the introduction of distributed and renewable energy based resources, a shift to a more distributed operation paradigm is emerging, overturning the conventional top-down design and operation principles. This shift creates a demand for distributed control systems (DCS) to facilitate a more adaptive and efficient operation of power networks. One key challenge here is to ensure the required reliability of distributed control systems. Whereas proven strategies exist for reliable control for coordination of physical actions, with increasing distribution of such control, the reliability and degradation properties in response to communications issues become more important. We build on the notion of Quality Choreographies, a formal model for the development of failure-aware distributed systems, and discuss how quality choreographies respond to the needs presented by DCS. We demonstrate their applicability by modelling the Bully Algorithm, one of the de-facto election algorithms used in coordination of DCS.

2016

PLACES

Type-checking Availability in Choreographic Programming López, Hugo A., Nielson, Flemming, and Nielson, Hanne Riis 2016 [Abstract] [Preprint]
Choreographic programming is a programming-language design approach that drives a safe protocol development in distributed systems. We study choreographic programming for loosely-coupled infrastructures, where the availability of components may change at runtime. We introduce a choreography language featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress
ArXiv

A Theory of Available-by-Design Communication Systems López, Hugo A., Nielson, Flemming, and Nielson, Hanne Riis CoRR 2016 [Abstract] [Publisher's copy]
Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Starting from a global specification (choreography) one can generate distributed implementations. The advantages of this top-down approach lie in the correctness-by-design principle, where implementations (endpoints) generated from a choreography behave according to the strict control flow described in the choreography, and do not deadlock. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where not all endpoints are always available. We introduce the Global Quality Calculus (GCq), a variant of choreographic programming for the description of communication systems where some of the components involved in a communication might fail. GCq features novel operators for multiparty, partial and collective communications. This paper studies the nature of failure-aware communication: First, we introduce GCq syntax, semantics and examples of its use. The interplay between failures and collective communications in a choreography can lead to choreographies that cannot progress due to absence of resources. In our second contribution, we provide a type system that ensures that choreographies can be realized despite changing availability conditions. A specification in GCq guides the implementation of distributed endpoints when paired with global (session) types. Our third contribution provides an endpoint-projection based methodology for the generation of failure-aware distributed processes. We show the correctness of the projection, and that well-typed choreographies with availability considerations enjoy progress.
FORTE

Enforcing Availability in Failure-Aware Communicating Systems López, Hugo A., Nielson, Flemming, and Nielson, Hanne Riis In Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2016 [Abstract] [Publisher's copy] [Preprint]
Choreographic programming is a programming-language design approach that drives error-safe protocol development in distributed systems. Motivated by challenging scenarios in Cyber-Physical Systems (CPS), we study how choreographic programming can cater for dynamic infrastructures where the availability of components may change at runtime. We introduce the Global Quality Calculus (GCq), a process calculus featuring novel operators for multiparty, partial and collective communications; we provide a type discipline that controls how partial communications refer only to available components; and we show that well-typed choreographies enjoy progress.

2015

PPDP

Declarative interpretations of session-based concurrency Cano, Mauricio, López, Hugo A., Pérez, Jorge A., and Rueda, Camilo In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14-16, 2015 2015 [Abstract] [Publisher's copy] [Preprint]
Session-based concurrency is a type-based approach to the analysis of communication-intensive systems. Correct behavior in these systems may be specified in an operational or declarative style: the former defines how interactions are structured; the latter defines governing conditions. In this paper, we investigate the relationship between operational and declarative models of session-based concurrency. We propose two interpretations of session π-calculus processes as declarative processes in linear concurrent constraint programming (lcc). They offer a basis on which both operational and declarative requirements can be specified and reasoned about. By coupling our interpretations with a type system for lcc, we obtain robust declarative encodings of π-calculus mobility.
OOPSLA

Protocol-based verification of message-passing parallel programs López, Hugo A., Marques, Eduardo R. B., Martins, Francisco, Ng, Nicholas, Santos, César, Vasconcelos, Vasco Thudichum, and Yoshida, Nobuko In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015 2015 [Abstract] [Publisher's copy] [Preprint]
We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.

2014

Type-Based Verification of Message-Passing Parallel Programs Vasconcelos, Vasco Thudichum, Martins, Francisco, Marques, Eduardo R. B., López, Hugo A., Santos, César, and Yoshida, Nobuko 2014 [Abstract] [Preprint]
We present a type-based approach to the verification of the communication structure of parallel programs. We model parallel imperative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, including point-to-point messages, broadcast, reduce, and array scatter and gather. The paper proposes a decidable dependent type system incorporating abstractions for the various communication operators, a form of primitive recursion, and collective choice. Term types may refer to values in the programming language, including integer, floating point and arrays. The paper further introduces a core programming language for imperative, message-passing, parallel programming, and shows that the language enjoys progress.

2013

2012

FIT

Refinement for Transition Systems with Responses Carbone, Marco, Hildebrandt, Thomas T., López, Hugo A., Perrone, Gian, and Wasowski, Andrzej In 4th. International Workshop on Foundations of Interface Technologies (FIT) 2012 [Preprint]
Ph.D. Thesis

López, H. A. (2012). Foundations of Communication-Centred Programming [PhD thesis]. IT University of Copenhagen. [Abstract] [Preprint]
Service and process-oriented systems are relatively new technologies that promise effective business processes and flexible and adaptable enterprise IT systems. The key factor in service systems is the ability to decompose a business process into a distributed system, where each participant implements parts of the functions in a business process, and interactions between participants are performed via message passing. In recent years, service- and process-oriented applications have rapidly become the norm for distributed enterprises and they have led to a number of new programming languages and standards, collectively referred to as communication-centred programming. Despite their adoption, these languages and standards for communication-centred programming are still young and unstable, and not grounded on a solid theoretical foundation. There are at least two significant dimensions when describing communication- centred programs: First, the global/local views used to describe interactions, and second, the imperative/declarative specifications styles used. With respect to views: a global view considers the system as a whole, describing specifications as sequences of message exchanges among participants, and a local view describes the system as a concurrent composition of processes, implementing each participant in the system. While the global view is what is usually provided as specification, the local view is a necessary step towards a distributed implementation. On specification styles: If processes are defined imperatively, then the control flow is defined explicitly (e.g.: as a flow graph of interactions/commands). In a declarative approach processes are described as a collection of conditions (e.g.: logical formulae) they should fulfil in order to be considered correct. Until now, research in these two dimensions have evolved rather independently from each other. This dissertation collects works devoted to foundational studies in communication- centred programming. Specifically, the dissertation revolves around process calculi as the main analytical tool for service-oriented systems. Process calculi are formal languages conceived for the description and analysis of concurrent systems, provid- ing a rigorous framework where distributed systems can be accurately analysed, by means of reasoning techniques to verify essential properties of a system. By means of process calculi, we provide formal relations between global and local views, and declarative/imperative specifications. This is achieved by extending previous works on the area with additional information in model specifications, like timing constraints and compensable behaviour. Finally, we provide process specifications with reason- ing techniques (specification logics, type systems, simulation techniques) that allow one to verify the behaviour of a service specification with respect to trustworthy properties in the system. Keywords: Process Calculi, Service-Oriented models, specification logics, type systems.
WS-FM

Time and Exceptional Behavior in Multiparty Structured Interactions López, Hugo A., and Pérez, Jorge A. In Web Services and Formal Methods - 8th International Workshop, WS-FM 2011, Clermont-Ferrand, France, September 1-2, 2011, Revised Selected Papers 2012 [Abstract] [Publisher's copy] [Preprint]
The Conversation Calculus (CC) is a model of multiparty interactions which extends the π-calculus with the notion of conversation—a possibly distributed medium in which participants may communicate. Here we study the interplay of time and exceptional behavior for models of structured communications based on conversations. We propose C3, a timed variant of the CC in which conversations feature both standard and exceptional behavior. The exceptional behavior may be triggered either by the passing of time (a timeout) or by an explicit signal for conversation abortion. By presenting a compelling example from a healthcare scenario, we argue that the combination of time and exceptional behavior leads to more meaningful models of structured communications

2011

NWPT

Open Mixed Refinement Carbone, Marco, Hildebrandt, Thomas, and López, Hugo A. In Nordic Workshop of Programming Theory (NWPT) 2011 [Preprint]
PLACES

Timed, Compensable Conversations López, Hugo A., and Pérez, Jorge A. In PLACES’11: Programming Language Approaches to Concurrency and Communication-cEntric Software 2011 [Abstract] [Preprint]
We are interested in the interplay of timing issues and exceptional behavior in the realm of structured communications. As an initial step, we have defined C 3 , a variant of the Conversation Calculus in which conversation contexts are enriched with a time duration, a compensating activity, and a designated signal for conversation abortion. In this note, we present C 3 and its basic semantics, and discuss ongoing work for equipping the language with logic-based reasoning techniques.

2010

PLACES

A Logic for Choreographies Carbone, Marco, Grohmann, Davide, Hildebrandt, Thomas T., and López, Hugo A. In Proceedings Third Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software, PLACES 2010, Paphos, Cyprus, 21st March 2010. 2010 [Abstract] [Publisher's copy] [Preprint]
We explore logical reasoning for the global calculus, a coordination model based on the notion of choreography, with the aim to provide a methodology for specification and verification of structured communications. Starting with an extension of Hennessy-Milner logic, we present the global logic (GL), a modal logic describing possible interactions among participants in a choreography. We illustrate its use by giving examples of properties on service specifications. Finally, we show that, despite GL is undecidable, there is a significant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.
ICLP-DC

Models for Trustworthy Service and Process Oriented Systems López, Hugo A. In Technical Communications of the 26th International Conference on Logic Programming, ICLP 2010, July 16-19, 2010, Edinburgh, Scotland, UK 2010 [Abstract] [Publisher's copy] [Preprint]
Service and process-oriented systems promise to provide more effective business and work processes and more flexible and adaptable enterprise IT systems. However, the technologies and standards are still young and unstable, making research in their theoretical foundations increasingly important. Our studies focus on two dichotomies: the global/local views of service interactions, and their imperative/declarative specification. A global view of service interactions describes a process as a protocol for interactions, as e.g. an UML sequence diagram or a WS-CDL choreography. A local view describes the system as a set of processes, e.g. specified as a π -calculus or WS-BPEL process, implementing each participant in the process. While the global view is what is usually provided as specification, the local view is a necessary step towards a distributed implementation. If processes are defined imperatively, the control flow is defined explicitly, e.g. as a sequence or flow graph of interactions/commands. In a declarative approach processes are described as a collection of conditions they should fulfill in order to be considered correct. The two approaches have evolved rather independently from each other. Our thesis is that we can provide a theoretical framework based on typed concurrent process and concurrent constraint calculi for the specification, analysis and verification of service and process oriented system designs which bridges the global and local view and combines the imperative and declarative specification approaches, and can be employed to increase the trust in the developed systems. This article describes our main motivations, results and future research directions.

2009

Jour.Mat.

Process Calculi to Analyze Emerging Applications in Concurrency Arbeláez, Alejandro, Aristizábal, Andrés, Gutiérrez, Julian, López, Hugo A., Pérez, Jorge A., Rueda, Camilo, and Valencia, Frank D. Matématicas: Enseñanza Universitaria 2009 [Abstract] [Preprint]
The notion of computation has significantly evolved in the last ten years or so. Modern computing systems (e.g., Internet) now exhibit infinite behavior, usually in the context of decentralized networks where interactions are inherently concurrent. The ubiqui- tous presence of this new kind of systems has led to the urgent need of counting with techniques for designing them in a reliable way. Process calculi are formal specification languages of concurrent systems in which the notions of process and interaction pre- vail. They are endowed with reasoning techniques that allow to rigorously determine whether a system exhibits some desirable properties. The generic nature of process calculi has made possible their successful application in very diverse areas. Based on recent work by the authors, this paper illustrates the use of process calculi in two emerging application areas: biology and security protocols. Basic notions of process calculi are introduced, real systems in the two areas are modeled and their properties are verified.
ICLP

Types for Secure Pattern Matching with Local Knowledge in Universal Concurrent Constraint Programming Hildebrandt, Thomas T., and López, Hugo A. In Logic Programming, 25th International Conference, ICLP 2009, Pasadena, CA, USA, July 14-17, 2009. Proceedings 2009 [Abstract] [Publisher's copy] [Preprint]
The fundamental primitives of Concurrent Constraint Programming (CCP), tell and ask, respectively adds knowledge to and infers knowledge from a shared constraint store. These features, and the elegant use of the constraint system to represent the abilities of attackers, make concurrent constraint programming and timed CCP (tcc) interesting candidates for modeling and reasoning about security protocols. However, they lack primitives for the communication of secrets (or local names as in the π -calculus) between agents. The recently proposed universal tcc (utcc) introduces a universally quantified ask operation that makes it possible to infer knowledge which is local to other agents. However, it allows agents to guess knowledge even if it is encrypted or communicated on secret channels, simply by quantifying over both the encryption key (or channel) and the message simultaneously. We present a secure utcc (utccs) based on: (i) a simple type system for constraints allowing to distinguish between restricted (secure) and non-restricted (universally quantifiable) variables in constraints, and (ii) a generalization of the universally quantified ask operation to allow the assumption of local knowledge. We illustrate the use of the utccs calculus with examples on communication of local names (as in the π -calculus) and for giving semantics to secure pattern matching in a prototypical security language. Key words:Concurrent Constraint Programming, Process Calculi, Type systems, Mobility, Security
PLACES

Towards a Unified Framework for Declarative Structured Communications López, Hugo A., Olarte, Carlos, and Pérez, Jorge A. In Proceedings Second International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2009, York, UK, 22nd March 2009. 2009 [Abstract] [Publisher's copy] [Preprint]
We present a unified framework for the declarative analysis of structured communications. By relying on a (timed) concurrent constraint programming language, we show that in addition to the usual operational techniques from process calculi, the analysis of structured communications can elegantly exploit logic-based reasoning techniques. We introduce a declarative interpretation of the language for structured communications proposed by Honda, Vasconcelos, and Kubo. Distinguishing features of our approach are: the possibility of including partial information (constraints) in the session model; the use of explicit time for reasoning about session duration and expiration; a tight correspondence with logic, which formally relates session execution and linear-time temporal logic formulas
MSc Thesis

López, H. A. (2009). Formal Models for Trustworthy Process and Service Oriented Systems [Master's thesis]. IT University of Copenhagen. [Abstract] [Preprint]
This report studies process calculi and its connections with service oriented systems. Despite of being such a young trend, service oriented systems have become an important area of research in the last decade, and several trends have been derived. In particular, we center our studies in the relationships between two dichotomies: the global/local views of services, and the imperative/declarative way used for the specification of services. On the one hand, the level of abstraction used for modelling processes plays an important role: either we describe an interaction scenario from a global viewpoint (choreography) or we describe the system as the composition of the local behaviours of each participant (orchestration). On the other hand, descriptions can have imperative or declarative flavors: In an imperative approach, we explicitly define the control flow of commands, whereas in a declarative approach the focus is drifted to the specification of the set of conditions processes should fulfill in order to be considered correct. Even if these two trends address similar concerns, we find that they have evolved rather independently from each other. The ultimate goals of this thesis are: (i) to provide formal models for process and service oriented systems, possibly combining the different views described above, and (ii) to provide support for the reasoning about correctness and security of a service oriented system, thereby raising its level of trustworthiness. Specifically, this project centers its research within the area of process calculi, and its connections with type systems and specification logics as ways to provide such correctness guarantees. The report can be divided into two main contributions: - First, we start by using a model of coordination defined in terms of agents that interact over a global store consulting and imposing constraints. The model, known as Concurrent Constraint Programming (CCP), allows for asynchronous communication, abstraction of data, deadlocks and a limited model of mobile behaviour. A recent extension to CCP, known as Universal Timed CCP (utcc) introduces the possibility of universally quantify over predicates in the constraint store. We propose a simple type system for constraints used as patterns in process abstractions, which essentially allows us to distinguish between universally abstractable information and secure (non-leakable information) in predicates. We also propose a novel notion of abstraction under local knowledge, which gives a general way to model that a process (principal) knows a key and can use it to decrypt a message encrypted with this key without revealing the key. - Second, we relate the work on Concurrent Constraint Programming to other models of coordination. We describe initial results on the definition of a formal framework for the declarative analysis of services. We shall exploit utcc, to give a declarative interpretation to the language defined by Honda, Vasconcelos, and Kubo (henceforth referred to as HVK). This way, services can be analyzed in a declarative framework where time is defined explicitly. We begin by proposing an encoding of the HVK language into utcc and studying its correctness. We then move to the timed setting, and propose HVKT , a timed extension of HVK. The extended language explicitly includes information on session duration, allows for declarative preconditions within session establishment constructs, and features a construct for session abortion. We then discuss how the encoding of HVK into utcc straightforwardly extends to HVKT . Additionally, we present initial efforts in relating logics and coordination models. We aim at leveraging the trustworthiness of a process model by providing a methodology for the specification and verification of structured communications. As recently presented, choreographies and orchestrations are operationally correspondent, and one can either use an choreography to generate its end-point projections, or to take a set of end-point specifications and describe their respective choreography. We present a way to describe properties over global specifications. Starting with an extension of Hennesy-Milner logic, we introduce a proof system that allows for verification of properties among participants in a choreography. With such a logic, one can see the state of a choreography as a formula, and one can check for satisfaction of desirable properties. Some examples of important properties on service specifications are drawn, and we provide hints on how this work can be extended towards a full verification framework for services, closing the gap between logics for choreography and their correspondent parts over an end-point projection.

2008

2007

SemSOC

Goal-Equivalent Secure Business Process Re-engineering López, Hugo A., Massacci, Fabio, and Zannone, Nicola In Service-Oriented Computing - ICSOC 2007 Workshops, International Workshops, Vienna, Austria, September 17, 2007, Revised Selected Papers 2007 [Abstract] [Publisher's copy] [Preprint]
The introduction of information technologies in health care systems often requires to re-engineer the business processes used to deliver care. Obviously, the new and re-engineered processes are observationally different and thus we cannot use existing model-based techniques to argue that they are somehow “equivalent”. In this paper we propose a method for passing from SI*, a modeling language for capturing and modeling functional, security, and trust organizational and system requirements, to business process specifications and vice versa. In particular, starting from an old secure business process, we reconstruct the functional and security requirements at organizational level that such a business process was supposed to meet (including the trust relations that existed among the members of the organization). To ensure that the re-engineered business process meets the elicited requirements, we employ a notion of equivalence based on goal-equivalence. Basically, we verify if the execution of the business process, described in terms of the trace it generates, satisfies the organizational model. We motivate and illustrate the method with an e-health case study.
MOTHIS

Goal-Equivalent Secure Business Process Re-engineering for E-Health López, Hugo A., Massacci, Fabio, and Zannone, Nicola In Model Based Trustworthy Health Information Systems (MOTHIS’07) 2007 [Abstract] [Preprint]
The introduction of ITs in e-Health often requires to re-engineer the business processes used to deliver care. Obviously the new and re-engineered processes are observationally different and thus we cannot use existing modelbased techniques to argue that they are somehow “equivalent”. In this paper we propose a notion of equivalence over secure business processes based on the notion of goal-equivalence: – start from the old secure business process; – reconstruct from that business process the functional and security requirements at organizational level that the old business process was supposed to meet (including the trust relations that existed among the members of the organization); – compare the re-engineered business process with the requirements and see if they are equally met or possibly improved. To this intent, we present a reasoning method for passing from SI*, a modeling language that captures the functional, security and trust requirements of IT systems and their operational environments, to business processes specifications and vice versa. Both translation processes are complementary, in the sense that SI* models can have multiple business process concretizations, and different business processes can be equivalent in terms of the goals they achieve. We illustrate and motivate the proposed approach using an e-health case study

2006

ICLP

A Declarative Framework for Security: Secure Concurrent Constraint Programming López, Hugo A., Palamidessi, Catuscia, Pérez, Jorge Andrés, Rueda, Camilo, and Valencia, Frank D. In Logic Programming, 22nd International Conference, ICLP 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings 2006 [Abstract] [Publisher's copy] [Preprint]
Due to technological advances such as the Internet and mobile computing, Security has become a serious challenge involving several disciplines of Computer Science. In recent years, there has been a growing interest in the analysis of security protocols and one promising approach is the development of formalisms that model communicating processes, in particular Process Calculi. The results are so far encouraging although most remains to be done.
TFIT

Formally reasoning about security issues in P2P protocols: A case study. Aristizábal, Andrés, López, Hugo A., Valencia, Frank D., and Rueda, Camilo In Third Taiwanese-French Conference on Information Technology (TFIT) 2006 [Abstract] [Preprint]
Peer-to-Peer (P2P) systems can be seen as highly dynamic distributed systems designed for very specific purposes, such as resources sharing in collaborative settings. Because of their ubiquity, it is fundamental to provide techniques for formally proving properties of the communication protocols underlying those systems. In this paper we present a formal specification of MUTE, a protocol for P2P systems, modelled in the SPL process calculus. Furthermore, we use the SPL reasoning techniques to show how the protocol enjoys a secrecy property against outsider attacks. By formally modeling and analyzing a real-world, yet informally specified protocol, we bear witness to the applicability of SPL as a formalism to specify security protocols as well as the flexibility of its reasoning techniques. This paper represents our first approach towards the use of process calculi, in particular SPL, for the specification and reasoning of P2P protocols.
BSc.Thesis

Aristizábal, A., & López, H. A. (2006). Using Process Calculi to model and Verify Security Properties in Real Communication Protocols [Master's thesis]. Pontificia Universidad Javeriana. [Abstract] [Preprint]
This work explores the use of concurrent process calculi in the analysis, design, specification and verification of communication protocols. In particular, it proposes the use of SPL as a process calculus well suited for the analysis and verification of security properties over Peer- to-Peer(P2P) systems. In this way, MUTE and FTN, two protocols that clearly represent the behavior of distributed communication systems over open networks, are modelled and verified in SPL. The first protocol portrays a general method for sharing resources over a dynamic network and the second is oriented to the dynamic reconfiguration of applications in collab- orative environments. Security properties relevant for each of these protocols are identified and analyzed by means of process calculi, bearing witness of the applicability of this kind of reasonings. This work is complemented with modified versions of the protocols, correcting the security holes encountered in previous versions. In addition, a set of encodings are modelled in SPL, easing the description of concurrent protocols specified in other approaches.

2005

ALP-newsletter

Using a Declarative Process Language for P2P Protocols Aristizábal, Andrés, López, Hugo A., and Rueda, Camilo The Association for Logic Programming (ALP) Newsletter Digest 2005 [Abstract] [Publisher's copy] [Preprint]
Peer-to-Peer (P2P) systems can be seen as highly dynamic distributed systems designed for very specific purposes, such as resources sharing in collaborative settings. Because of their ubiquity, it is fundamental to provide techniques for formally proving properties of the communication protocols underlying those systems. In this paper we present a formal model of MUTE, a protocol for P2P systems, in the SPL; a specification language with a striking resemblance to Concurrent Constraint Programming. Furthermore, we use the SPL reasoning techniques to show the protocol enjoys a secrecy property againts outsider attacks. By formally modeling and analyzing a popular (albeit never specified) protocol, we bear witness to the applicability of SPL as a formalism to model and reason about security protocols as well as flexibility of the its reasoning techniques.