Listar por

Por fecha de publicación Autores Títulos Materias Tipo de Material

El grupo de investigación CTG-informática es un grupo interdisciplinario que se interesa en la ciencia, gestión e innovación en informática. Con especial interés en resolver y apoyar con tecnología que aumente la productividad a las organizaciones en su estrategia de negocio, contribuyendo así al desarrollo del país en la sociedad del conocimiento.

Novedades

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.

Envíos recientes

Improving hardware/software interface management in systems of systems through documentation as code

Cadavid, Héctor; Andrikopoulos, Vasilios; Avgeriou, Paris (SpringerEstados Unidos, 2023)

Context: The management of Interface Control Documents (ICDs) has shown to be a major pain point in the architecting processes of Systems of Systems (SoS). Objective ThisworkaimstoimproveonpreviouslyidentifiedICDmanagem ...
Monitoring the Quality and Perception of Service in Colombian Public Service Companies with Twitter and Descriptive Temporal Analysis

Conti, Dante; Gomez, Carlos Eduardo; Jaramillo, Juan Guillermo; Ospina, Victoria Eugenia (MDPI (Multidisciplinary Digital Publishing Institute)Basel (Suiza), 2023)

The main goal of this research is to analyze the perception of service in public sector companies in the city of Bogota via Twitter and text mining to identify areas, problems, and topics aiming for quality service ...
A taxonomy of tools and approaches for distributed genomic analyses

Garzón, Wilmer; Benavides, Luis Alberto; Gignard, Alban; Südholt, Mario (Elsevier LtdBogotá (Colombia), 2022)

The amount of biomedical data collected and stored has grown significantly. Analyzing these extensive amounts of data cannot be done by individuals or single organizations anymore. Thus, the scientific community is creating ...
Evaluación de la percepción de los servicios públicos en Colombia mediante Text Mining vía Twitter

Gómez Rivera, Carlos Eduardo; Conti, Dante; Jaramillo Yepes, Juan Gullermo; Ospina Becerra, Victoria Eugenia (Universidad Politécnica de CataluñaUniversidad Autónoma de SinaloaEspaña, 2022)

En Bogotá, los prestadores de servicios básicos son: Enel, Vanti y El acueducto, grandes empresas del sector que deben caracterizarse por una operación customer centricity. Sin embargo, dado que estas compañías son las que ...
Documentation-as-code for Interface Control Document Management in Systems of Systems: a Technical Action Research Study

Cadavid, Héctor; Andrikopoulos, Vasilios; Avgeriou, Paris (SpringerEstados Unidos, 2022)

The architecting of Systems of Systems (SoS), that is, of systems that emerge from the cooperation of multiple independent constituent systems, is a topic of increasing interest in both industry and academia. However, ...
System- and Software-level Architecting Harmonization Practices for Systems-of-Systems: An exploratory case study on a long-running large-scale scientific instrument

Cadavid, Héctor; Andrikopoulos, Vasilios; Avgeriou, Paris; Broekema, Chris (Elsevier SciencePaíses Bajos, 2022)

The problems caused by the gap between systemand software-level architecting practices, especially in the context of Systems of Systems where the two disciplines inexorably meet, is a well known issue with a disappointingly ...
Neural network-based optimization of fibres for seismic retrofitting applications of UHPFRC

Abellán García, Joaquín; DSánchez Díaz, Jairo A.; Ospina Becerra, Victoria Eugenia (Taylor & FrancisReino Unido, 2021)

Ultra-high-performance fibre reinforced concrete (UHPFRC) is an advanced construction material that provides new opportunities in the future of the construction industry around the world. Among those new applications, ...
Mediation System for cooperative activities: knowledge system design

Ospina-Becerra, Victoria Eugenia; Fougères, Alain-Jérôme (WSEAS, 2008)

In this article we present the use the knowledge for a Mediation System, developed to give support to mechanical system designer activities. The use of cooperative systems must contain a sufficient level of assistance to ...
Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

Bohórquez, Jaime (University of Notre Dame, 2008)

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert’s style of proof and Gentzen’s deductive systems. In this context we call it CED ...
AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS

Fougères, Alain-Jérôme; Ospina-Becerra, Victoria Eugenia (In CognitoFrance, 2009)

Nous présentons, dans cet article, deux concepts pour améliorer l'assistance à la coopération en conception de systèmes mécaniques : 1) le concept de micro-outils développé pour assister l'activité elle-même des concepteurs ...
Agent-Based Mediation System to Facilitate Cooperation in Distributed Design

Ospina-Becerra, Victoria Eugenia; Fougères, Alain-Jérôme (WSEASE.E.U.U., 2009)

In this article we present the use of knowledge for a Mediation System, developed to give support to participants in mechanical-system-designer activities. To use a cooperative system sufficient assistance is needed to ...
La inteligencia de negocios, un concepto informático

Oramas, Joaquin (ACISColombia, 2009)

Diferente a lo que podría esperarse, el concepto de Business Intelligence no es un resultado de desarrollos en el mundo de las Ciencias Administrativas, sino que es un producto del progreso de la Informática o de ...
An Inductive Theorem on the Correctness of General Recursive Programs

Bohórquez, Jaime (Oxford University Press, 2007)

We prove a relatively simple inductive theorem (analogous to Floyd and Dijkstra's Invariance Theorem for iterative programs) to verify the correctness of an ample class of non-deterministic general recursive programs. This ...
Theorem Proving Modulo Based on Boolean Equational Procedures

Rocha, Camilo; Meseguer, José (Springer, 2008)

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean ...
An elementary and unified approach to program correctness

Bohórquez, Jaime (Springer, 2009)

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra’s iterative style of programming ...
Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas

Cadavid Rengifo, Héctor Fabio; Gómez Perdomo, Jonatan (ScieloColombia, 2009)

En este artículo se describe un sistema desarrollado para la extracción de grandes cuerpos de texto de Internet, teniendo como motivación el valor que ofrecen los ejemplos de lenguaje natural disponibles en la red para ...
Rewriting Logic Semantics of a Plan Execution Language

Dowek, Gilles; Muñoz, César; Rocha, Camilo (E.E.U.U., 2010)

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a ...
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

Rocha, Camilo; Meseguer, José (SpringerBerlín, 2010)

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite ...
A formal library of set relations and its application to synchronous languages

Rocha, Camilo; Muñoz, César; Dowek, Gilles (Elsevier B.V., 2011)

Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and ...
Simulation and Verification of Synchronous Set Relations in Rewriting Logic

Rocha, Camilo; Múñoz, César (NASA Langley Research CenterHampton, Virginia., 2011)

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract ...

Más

Envíos recientes

AD - CTG – Informática
...
|

Clasificación B- Convocatoria 2018

LEER
Improving hardware/software interface management in systems of systems through documentation as code
...
Cadavid, Héctor | 2023

Context: The management of Interface Control Documents (ICDs) has shown to be a major pain point in the architecting processes of Systems of Systems (SoS). Objective ThisworkaimstoimproveonpreviouslyidentifiedICDmanagementissuesusing the documentation-as-code philosophy as a potential basis for a treatment, and in collaboration with practitioners. Method: Weconducted a Technical Action Research (TAR) study with a group of engineers at the Netherlands Radio Astronomy Institute (ASTRON), in the context of the LOFAR radio telescope. An additional research instrument, in the form of an expert panel, was used to evaluate the transferability of the proposed treatment to alternative domains. Results: In-depth insights on previously identified interface management issues were gained. Based on these insights a functional proof-of-concept was developed aimed at addressing these issues following the documentation-as-code principles. In addition to receiving overall positive reviews from practitioners and experts, further areas of improvement and transferability considerations for future work were identified. Conclusions: The proposed approach, which to our knowledge has not been explored before in this context, is promising to address some of the recurring interfacing-related issues with directed SoS in multiple engineering domains. This could be done mainly by enforcing consistency and completeness on both text-based and formal elements of the ICDs, and turning ICDs into single sources of truth for the architecting processes of large scale SoS.

LEER
Monitoring the Quality and Perception of Service in Colombian Public Service Companies with Twitter and Descriptive Temporal Analysis
...
Conti, Dante | 2023

The main goal of this research is to analyze the perception of service in public sector companies in the city of Bogota via Twitter and text mining to identify areas, problems, and topics aiming for quality service improvement. To achieve this objective, a structured method for data modeling is implemented based on the KDD methodology. Tweets from January to June 2022 related to the companies in the sector are processed, and a temporal analysis of the evolution of sentiment is performed based on the dictionaries Bing, AFINN, and NRC. Subsequently, the LDA algorithm (Latent Dirichlet Allocation algorithm) is used to visually identify the topics with the greatest negative impact reported by the users in each of the 6 months by adding the temporal dimension. The results revealed that, for Aqueduct (water supply service), the topic with the highest dissatisfaction is related to the “Water Tank Request” processes; for Enel (energy services) “Service Outages”; and for Vanti (gas services), “Case solution and request information”. Temporal patterns of tweets, sentiments, and topics are also highlighted for the three companies.

LEER
A taxonomy of tools and approaches for distributed genomic analyses
...
Garzón, Wilmer | 2022

The amount of biomedical data collected and stored has grown significantly. Analyzing these extensive amounts of data cannot be done by individuals or single organizations anymore. Thus, the scientific community is creating global collaborative efforts to analyze these data. However, biomedical data is subject to several legal and socio- economic restrictions hindering the possibilities for research collaboration. In this paper, we argue that researchers require new tools and techniques to address the restrictions and needs of global scientific collaborations over geo-distributed biomedical data. These tools and techniques must support what we call Fully Distributed Collaborations (FDC), which are research endeavors that harness means to exploit and analyze massive biomedical information collaboratively while respecting legal and socio-economical restrictions. This paper first motivates and discusses the requirements of FDCs in the context of a research collaboration on the development of diagnostic and predictive tools for the risk of intracranial aneurysm formation and rupture (the ICAN project). The paper then presents a taxonomy classifying the current tools and techniques for biomedical analysis with respect to the proposed requirements. The taxonomy considers three key architectural features to support FDC scenarios: data and computation placement, Privacy and Security, and Performance and Scalability. The review reveals new research opportunities to design tools and techniques for multi-site analyses encouraging scientific collaborations while mitigating technical and legal constraints.

LEER
Evaluación de la percepción de los servicios públicos en Colombia mediante Text Mining vía Twitter
...
Gómez Rivera, Carlos Eduardo | 2022

En Bogotá, los prestadores de servicios básicos son: Enel, Vanti y El acueducto, grandes empresas del sector que deben caracterizarse por una operación customer centricity. Sin embargo, dado que estas compañías son las que mayor cantidad de quejas y reclamos presentan ante los entes regulatorios, la percepción del servicio puede no ser la mejor. Determinar la veracidad de esto, es el objetivo de la presente investigación, a través de la explotación de técnicas de minería de texto aprovechando la voz de cliente en los tuits de los usuarios; aplicando la metodología Knowledge Discovery in Databases, para generar la base de datos compuesta por 9071 tuits de las tres empresas. En la fase de limpieza de datos, se establecen pasos adicionales para refinar dicha base y consolidar los tuits de interés para la investigación. Lo anterior, permite obtener una explotación de los datos explicando los resultados a través de nubes de palabras, diagramas de frecuencia, análisis de sentimientos y los ratios entre la polaridad de los tuits. Los resultados permiten inferir que, para la ventana de tiempo en el cual se realiza el análisis, la percepción del servicio no es buena y que existen oportunidades de mejora para las tres compañías.

LEER
Documentation-as-code for Interface Control Document Management in Systems of Systems: a Technical Action Research Study
...
Cadavid, Héctor | 2022

The architecting of Systems of Systems (SoS), that is, of systems that emerge from the cooperation of multiple independent constituent systems, is a topic of increasing interest in both industry and academia. However, recent empirical studies revealed what seems to be an overlooked aspect of the architecting of SoS that is linked to major integration and operational issues: the interplay between the various disciplines involved in such an architecting process. This aspect becomes particularly relevant for the management of the interfaces between the SoS constituents, where such disciplines inevitably meet. In this paper, we present the results of the f irst cycle of a Technical Action Research (TAR) study conducted in cooperation between the authors and a group of practitioners involved in the long-running architecting process of a largescale radio astronomy SoS project. This TAR is aimed at exploring potential improvements of the document-centered interface management approach currently followed in this project by adopting elements of the documentation-as-code philosophy, which is widely adopted in the domain of software systems. As a result, a working proof-of-concept of an ICD (Interface Control Document) management approach was developed by the researchers and evaluated by the practitioners. The results of the study and the corresponding lessons learned are reported in this work.

LEER
System- and Software-level Architecting Harmonization Practices for Systems-of-Systems: An exploratory case study on a long-running large-scale scientific instrument
...
Cadavid, Héctor | 2022

The problems caused by the gap between systemand software-level architecting practices, especially in the context of Systems of Systems where the two disciplines inexorably meet, is a well known issue with a disappointingly low amount of works in the literature dedicated to it. At the same time, organizations working on Systems of Systems have been developing solutions for closing this gap for many years now. This work aims to extract such knowledge from practitioners by studying the case of a large-scale scientific instrument, a geographically distributed radio telescope to be more specific, developed as a sequence of projects during the last two decades. As the means for collecting data for this study we combine online interviews with a virtual focus group of practitioners from the organization responsible for building the instrument. Through this process, we identify persisting problems and the best practices that have been developed to deal with them, together with the perceived benefits and drawbacks of applying the latter in practice. Some of our major findings include the need to avoid over-reliance on the flexibility of software to compensate for incomplete requirements, hidden assumptions, as well as late involvement of system architecting, and to facilitate the cooperation between the involved disciplines through dedicated architecting roles and the adoption of unifying practices and standards.

LEER
Neural network-based optimization of fibres for seismic retrofitting applications of UHPFRC
...
Abellán García, Joaquín | 2021

Ultra-high-performance fibre reinforced concrete (UHPFRC) is an advanced construction material that provides new opportunities in the future of the construction industry around the world. Among those new applications, rehabilitation, and seismic retrofitting of existing damaged or non-ductile concrete structures can be highlighted. The main objective of this paper is to optimise the hybrid blend of fibres that allows a previously optimised eco-friendly ultra-high performance cementitious paste to achieve the ductility requirements for seismic retrofitting applications at lower costs. To meet this goal, two artificial neural network models (ANNs) were created to predict the energy absorption capacity (g) and maximum post-cracking strain (epc). A total of 50 own experimental campaign data added to 550 published works throughout the world data were used for training purposes by using the R-code language. Once the models were trained and validated, a multi-objective optimisation was used to select the combination of fibres that achieved the limit values of g 50kJ/m3 and epc 0.3% considering cost constraints. The experimentally validated results indicated that the adequate blend of high strength steel micro-fibres and hooked end normal strength steel fibres fulfil the threshold values at a lower cost.

LEER
Mediation System for cooperative activities: knowledge system design
...
Ospina-Becerra, Victoria Eugenia | 2008

In this article we present the use the knowledge for a Mediation System, developed to give support to mechanical system designer activities. The use of cooperative systems must contain a sufficient level of assistance to facilitate and coordinate the actor’s activities. To accomplish this goal we introduce an artificial actor: the Mediator. To illustrate our approach we will present the specification of the knowledge of the Mediation System.

LEER
Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction
...
Bohórquez, Jaime | 2008

Dijkstra and Scholten have proposed a formalization of classical predicate logic on a novel deductive system as an alternative to Hilbert’s style of proof and Gentzen’s deductive systems. In this context we call it CED (Calculus of Equational Deduction). This deductive method promotes logical equivalence over implication and shows that there are easy ways to prove predicate formulas without the introduction of hypotheses or metamathematical tools such as the deduction theorem. Moreover, syntactic considerations (in Dijkstra’s words, “letting the symbols do the work”) have led to the “calculational style,” an impressive array of techniques for elegant proof constructions. In this paper, we formalize intuitionistic predicate logic according to CED with similar success. In this system (I-CED), we prove Leibniz’s principle for intuitionistic logic and also prove that any (intuitionistic) valid formula of predicate logic can be proved in I-CED.

LEER
AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS
...
Fougères, Alain-Jérôme | 2009

Nous présentons, dans cet article, deux concepts pour améliorer l'assistance à la coopération en conception de systèmes mécaniques : 1) le concept de micro-outils développé pour assister l'activité elle-même des concepteurs et 2) le concept de système de médiation introduit pour faciliter la coopération des concepteurs. Un micro-outil est destiné à une tâche bien identifiée, dont il va faciliter ou améliorer l'exécution, tout en laissant à son utilisateur toute latitude dans l'organisation de son activité à une échelle plus globale. Pour supporter l'usage des micro-outils nous avons développé une plate-forme agent (PLACID : Plate-forme Logiciel d'Aide à la Conception Innovante et Distribuée). Celle-ci apporte une assistance au travail de co-conception, guidé ou non par des processus complexes de type workflow. L'utilisation de systèmes coopératifs doit comporter un niveau suffisant d'assistance pour faciliter et coordonner l'activité des acteurs (réalisation de tâches et résolution collective de problèmes). Pour cela nous introduisons dans les interrelations coopératives des acteurs un acteur artificiel, le Médiateur (ou système de médiation), dont le rôle est de servir d'intermédiaire de coopération. Ce rôle s'avère des plus pertinents lorsque les acteurs sont engagés dans des situations de travail coopératif distantes. Dans l'intention d'illustrer notre approche nous présentons la conception des micro-outils et du système de médiation que nous avons intégrés dans un atelier coopératif d'analyse fonctionnelle technique (l'atelier MO-AFT).

LEER
Agent-Based Mediation System to Facilitate Cooperation in Distributed Design
...
Ospina-Becerra, Victoria Eugenia | 2009

In this article we present the use of knowledge for a Mediation System, developed to give support to participants in mechanical-system-designer activities. To use a cooperative system sufficient assistance is needed to facilitate and coordinate actors’ activities. To accomplish this goal we introduce an artificial actor: Mediator.The Mediator forms part of the group of collaborative, with the specific role of facilitating the cooperative activity. This role of assistance, differentiate the Mediator from other actors. This one is endowed with specific skills of cooperation (communication; awareness, coordination, co-memorization), requiring some acquired knowledge, which allow them to give assistance to the human actors. We will define the types of knowledge defined for our proposed Mediation System. Then we will illustrate the use of memorized knowledge by the Mediator during an activity of technical functional analysis.

LEER
La inteligencia de negocios, un concepto informático
...
Oramas, Joaquin | 2009

Diferente a lo que podría esperarse, el concepto de Business Intelligence no es un resultado de desarrollos en el mundo de las Ciencias Administrativas, sino que es un producto del progreso de la Informática o de la recientemente denominada “infotecnología”.

LEER
An Inductive Theorem on the Correctness of General Recursive Programs
...
Bohórquez, Jaime | 2007

We prove a relatively simple inductive theorem (analogous to Floyd and Dijkstra's Invariance Theorem for iterative programs) to verify the correctness of an ample class of non-deterministic general recursive programs. This result is based on Hoare and Jifeng's relational semantics. By considering the structure of its code and specification, we propose regularity conditions on the predicate transformer associated to the fixed-point equation of a general (non deterministic) recursive program to prove it correct by induction on a well founded ordering of a covering of the domain of its corresponding input-output relation. All fixed point solutions associated to a predicate transformer satisfying these regularity conditions coincide when restricted to the domain of its least fixed point solution. We find these conditions non unduly restrictive, since continuous operators defining deterministic programs as their corresponding least fixed-point solutions must fulfill them. We couch deterministic programs (viewed as least solutions of fixed-point equations) in a restriction of Hoare and Jifeng's P programming language of (partial) finitary relations into the greatest solutions of fixed-point equations expressed in terms of “total finitary” relations of an adequate restriction of their D language

LEER
Theorem Proving Modulo Based on Boolean Equational Procedures
...
Rocha, Camilo | 2008

Deduction with inference rules modulo computation rules plays an important role in automated deduction as an effective method for scaling up. We present four equational theories that are isomorphic to the traditional Boolean theory and show that each of them gives rise to a Boolean decision procedure based on a canonical rewrite system modulo associativity and commutativity. Then, we present two modular extensions of our decision procedure for Dijkstra-Scholten propositional logic to the Sequent Calculus for First Order Logic and to the Syllogistic Logic with Complements of L. Moss. These extensions take the form of rewrite theories that are sound and complete for performing deduction modulo their equational parts and exhibit good mechanization properties. We illustrate the practical usefulness of this approach by a direct implementation of one of these theories in Maude rewriting logic language, and automatically proving a challenge benchmark in theorem proving.

LEER
An elementary and unified approach to program correctness
...
Bohórquez, Jaime | 2009

We present through the algorithmic language DHL (Dijkstra-Hehner language), a practical approach to a simple first order theory based on calculational logic, unifying Hoare and Dijkstra’s iterative style of programming with Hehner’s recursive predicative programming theory, getting the “best of the two worlds” and without having to recur in any way to higher-order approaches such as predicate transformers, Hoare logic, fixed-point or relational theory.

LEER
Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas
...
Cadavid Rengifo, Héctor Fabio | 2009

En este artículo se describe un sistema desarrollado para la extracción de grandes cuerpos de texto de Internet, teniendo como motivación el valor que ofrecen los ejemplos de lenguaje natural disponibles en la red para las tareas de aprendizaje no supervisado de dichos naturales, dado por características como su enorme volumen, permanente actualización respecto de las alteraciones del lenguaje, y bajo costo, en tiempo y recursos, en cuanto a los mecanismos tradicionales de construcción de corpus para esas tareas de aprendizaje. Se presentan las estrategias incorporadas al sistema con el fin de maximizar el aprovechamiento de los recursos de hardware y así reducir los tiempos de extracción, al igual que se presentan las características de extensibilidad para los formatos soportados, y adaptabilidad respecto a la manera como el sistema limpia los contenidos para obtener muestras de lenguaje natural puras. Al final del artículo se presentan los resultados experimentales obtenidos con uno de los dominios de contenido en español más grande de Internet: es.wikipedia.org, a través de los cuales se concluye sobre la validez y aplicabilidad de un corpus extraído directamente de la Internet para un eventual proceso de aprendizaje de morfología o sintaxis.

LEER
Rewriting Logic Semantics of a Plan Execution Language
...
Dowek, Gilles | 2010

The Plan Execution Interchange Language (PLEXIL) is a synchronous language developed by NASA to support autonomous spacecraft operations. In this paper, we propose a rewriting logic semantics of PLEXIL in Maude, a high-performance logical engine. The rewriting logic semantics is by itself a formal interpreter of the language and can be used as a semantic benchmark for the implementation of PLEXIL executives. The implementation in Maude has the additional benefit of making available to PLEXIL designers and developers all the formal analysis and verification tools provided by Maude. The formalization of the PLEXIL semantics in rewriting logic poses an interesting challenge due to the synchronous nature of the language and the prioritized rules defining its semantics. To overcome this difficulty, we propose a general procedure for simulating synchronous set relations in rewriting logic that is sound and, for deterministic relations, complete. We also report on two issues at the design level of the original PLEXIL semantics that were identified with the help of the executable specification in Maude.

LEER
Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories
...
Rocha, Camilo | 2010

Sufficient completeness has been throughly studied for equational specifications, where function symbols are classified into constructors and defined symbols. But what should sufficient completeness mean for a rewrite theory R=(Σ,E,R) with equations E and non-equational rules R describing concurrent transitions in a system? This work argues that a rewrite theory naturally has two notions of constructor: the usual one for its equations E, and a different one for its rules R. The sufficient completeness of constructors for the rules R turns out to be intimately related with deadlock freedom, i.e., R has no deadlocks outside the constructors for R. The relation between these two notions is studied in the setting of unconditional order-sorted rewrite theories. Sufficient conditions are given allowing the automatic checking of sufficient completeness, deadlock freedom, and other related properties, by propositional tree automata modulo equational axioms such as associativity, commutativity, and identity. They are used to extend the Maude Sufficient Completeness Checker from the checking of equational theories to that of both equational and rewrite theories. Finally, the usefulness of the proposed notion of constructors in proving inductive theorems about the reachability rewrite relation →R associated to a rewrite theory R (and also about the joinability relation ↓R ) is both characterized and illustrated with an example.

LEER
A formal library of set relations and its application to synchronous languages
...
Rocha, Camilo | 2011

Set relations are particularly suitable for specifying the small-step operational semantics of synchronous languages. In this paper, a formal library of set relations for the definition, verification of properties, and execution of binary set relations is presented. The formal library consists of a set of theories written in the Prototype Verification System (PVS) that contains definitions and proofs of properties, such as determinism and compositionality, for synchronous relations. The paper also proposes a serialization procedure that enables the simulation of synchronous set relations via set rewriting systems. The library and the serialization procedure are illustrated with the rewriting logic semantics of the Plan Execution Interchange Language (PLEXIL), a rich synchronous plan execution language developed by NASA to support autonomous spacecraft operations.

LEER
Simulation and Verification of Synchronous Set Relations in Rewriting Logic
...
Rocha, Camilo | 2011

This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property verification of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm verification techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the verification of temporal properties of a synchronous system.

LEER

‹›

AD - CTG – Informática

Listar por

Novedades

Envíos recientes

Improving hardware/software interface management in systems of systems through documentation as code ﻿

Monitoring the Quality and Perception of Service in Colombian Public Service Companies with Twitter and Descriptive Temporal Analysis ﻿

A taxonomy of tools and approaches for distributed genomic analyses ﻿

Evaluación de la percepción de los servicios públicos en Colombia mediante Text Mining vía Twitter ﻿

Documentation-as-code for Interface Control Document Management in Systems of Systems: a Technical Action Research Study ﻿

System- and Software-level Architecting Harmonization Practices for Systems-of-Systems: An exploratory case study on a long-running large-scale scientific instrument ﻿

Neural network-based optimization of fibres for seismic retrofitting applications of UHPFRC ﻿

Mediation System for cooperative activities: knowledge system design ﻿

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction ﻿

AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS ﻿

Agent-Based Mediation System to Facilitate Cooperation in Distributed Design ﻿

La inteligencia de negocios, un concepto informático ﻿

An Inductive Theorem on the Correctness of General Recursive Programs ﻿

Theorem Proving Modulo Based on Boolean Equational Procedures ﻿

An elementary and unified approach to program correctness ﻿

Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas ﻿

Rewriting Logic Semantics of a Plan Execution Language ﻿

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories ﻿

A formal library of set relations and its application to synchronous languages ﻿

Simulation and Verification of Synchronous Set Relations in Rewriting Logic ﻿

Envíos recientes

AD - CTG – Informática

Improving hardware/software interface management in systems of systems through documentation as code

Monitoring the Quality and Perception of Service in Colombian Public Service Companies with Twitter and Descriptive Temporal Analysis

A taxonomy of tools and approaches for distributed genomic analyses

Evaluación de la percepción de los servicios públicos en Colombia mediante Text Mining vía Twitter

Documentation-as-code for Interface Control Document Management in Systems of Systems: a Technical Action Research Study

System- and Software-level Architecting Harmonization Practices for Systems-of-Systems: An exploratory case study on a long-running large-scale scientific instrument

Neural network-based optimization of fibres for seismic retrofitting applications of UHPFRC

Mediation System for cooperative activities: knowledge system design

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS

Agent-Based Mediation System to Facilitate Cooperation in Distributed Design

La inteligencia de negocios, un concepto informático

An Inductive Theorem on the Correctness of General Recursive Programs

Theorem Proving Modulo Based on Boolean Equational Procedures

An elementary and unified approach to program correctness

Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas

Rewriting Logic Semantics of a Plan Execution Language

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

A formal library of set relations and its application to synchronous languages

Simulation and Verification of Synchronous Set Relations in Rewriting Logic

Improving hardware/software interface management in systems of systems through documentation as code

Monitoring the Quality and Perception of Service in Colombian Public Service Companies with Twitter and Descriptive Temporal Analysis

A taxonomy of tools and approaches for distributed genomic analyses

Evaluación de la percepción de los servicios públicos en Colombia mediante Text Mining vía Twitter

Documentation-as-code for Interface Control Document Management in Systems of Systems: a Technical Action Research Study

System- and Software-level Architecting Harmonization Practices for Systems-of-Systems: An exploratory case study on a long-running large-scale scientific instrument

Neural network-based optimization of fibres for seismic retrofitting applications of UHPFRC

Mediation System for cooperative activities: knowledge system design

Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction

AIDE À LA CONCEPTION COLLABORATIVE. UN SYSTEME DE MEDIATION POUR L'USAGE DE MICRO- OUTILS LOGICIELS

Agent-Based Mediation System to Facilitate Cooperation in Distributed Design

La inteligencia de negocios, un concepto informático

An Inductive Theorem on the Correctness of General Recursive Programs

Theorem Proving Modulo Based on Boolean Equational Procedures

An elementary and unified approach to program correctness

Sistema de extracción de cuerpos de texto de la web para tareas lingüísticas

Rewriting Logic Semantics of a Plan Execution Language

Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories

A formal library of set relations and its application to synchronous languages

Simulation and Verification of Synchronous Set Relations in Rewriting Logic