A formal model of the Semantic Web Service Ontology (WSMO)

Semantic Web Service, one of the most significant research areas within the Semantic Web vision, has attracted increasing attention from both the research community and industry. The Web Service Modelling Ontology (WSMO) has been proposed as an enabling framework for the total/partial automation of the tasks (e.g., discovery, selection, composition, mediation, execution, monitoring, etc.) involved in both intra- and inter-enterprise integration of Web services. To support the standardisation and tool support of WSMO, a formal model of the language is highly desirable. As several variants of WSMO have been proposed by the WSMO community, which are still under development, the syntax and semantics of WSMO should be formally defined to facilitate easy reuse and future development. In this paper, we present a formal Object-Z formal model of WSMO, where different aspects of the language have been precisely defined within one unified framework. This model not only provides a formal unambiguous model which can be used to develop tools and facilitate future development, but as demonstrated in this paper, can be used to identify and eliminate errors present in existing documentation.

RELAX:a language to address uncertainty in self-adaptive systems requirement

Self-adaptive systems have the capability to autonomously modify their behavior at run-time in response to changes in their environment. Self-adaptation is particularly necessary for applications that must run continuously, even under adverse conditions and changing requirements; sample domains include automotive systems, telecommunications, and environmental monitoring systems. While a few techniques have been developed to support the monitoring and analysis of requirements for adaptive systems, limited attention has been paid to the actual creation and specification of requirements of self-adaptive systems. As a result, self-adaptivity is often constructed in an ad-hoc manner. In order to support the rigorous specification of adaptive systems requirements, this paper introduces RELAX, a new requirements language for self-adaptive systems that explicitly addresses uncertainty inherent in adaptive systems. We present the formal semantics for RELAX in terms of fuzzy logic, thus enabling a rigorous treatment of requirements that include uncertainty. RELAX enables developers to identify uncertainty in the requirements, thereby facilitating the design of systems that are, by definition, more flexible and amenable to adaptation in a systematic fashion. We illustrate the use of RELAX on smart home applications, including an adaptive assisted living system.

Semantic search components:a blueprint for effective query language interfaces

Formulating complex queries is hard, especially when users cannot understand all the data structures of multiple complex knowledge bases. We see a gap between simplistic but user friendly tools and formal query languages. Building on an example comparison search, we propose an approach in which reusable search components take an intermediary role between the user interface and formal query languages.

Informational Model of Natural Language Processing

The formal model of natural language processing in knowledge-based information systems is considered. The components realizing functions of offered formal model are described.

A Metaontology for Medical Diagnostics of Acute Diseases. Part 2. A Formal Description of Cause-and-effect Relations

This article is the continuation of the formal description of the metaontology for medical diagnostics in the language of applied logic. It contains a description of interrelations between terms of knowledge and reality in the form of ontological agreements.

A Metaontology for Medical Diagnostics of Acute Diseases. Part 3. A Formal Description of the Causes of Signs’ Values and of Diseases

This article is the final part of the formal description of the metaontology for medical diagnostics in the language of applied logic. It contains a description of the causes of signs’ values and of the causes of diseases.

Online Dictionary - Tool for Preservation of Language Heritage

The paper aims to represent a bilingual online dictionary as a useful tool helping preservation of the natural languages. The author focuses on the approach that was taken to develop compatible bilingual lexical database for the Bulgarian-Polish online dictionary. A formal model for the dictionary encoding is developed in accordance with the complex structures of the dictionary entries. These structures vary depending on the grammatical characteristics of Bulgarian headwords. The Web-application for presentation of the bilingual dictionary is also describred.

A framework for transforming, analyzing, and realizing software designs in unified modeling language

Unified Modeling Language (UML) is the most comprehensive and widely accepted object-oriented modeling language due to its multi-paradigm modeling capabilities and easy to use graphical notations, with strong international organizational support and industrial production quality tool support. However, there is a lack of precise definition of the semantics of individual UML notations as well as the relationships among multiple UML models, which often introduces incomplete and inconsistent problems for software designs in UML, especially for complex systems. Furthermore, there is a lack of methodologies to ensure a correct implementation from a given UML design. The purpose of this investigation is to verify and validate software designs in UML, and to provide dependability assurance for the realization of a UML design.^ In my research, an approach is proposed to transform UML diagrams into a semantic domain, which is a formal component-based framework. The framework I proposed consists of components and interactions through message passing, which are modeled by two-layer algebraic high-level nets and transformation rules respectively. In the transformation approach, class diagrams, state machine diagrams and activity diagrams are transformed into component models, and transformation rules are extracted from interaction diagrams. By applying transformation rules to component models, a (sub)system model of one or more scenarios can be constructed. Various techniques such as model checking, Petri net analysis techniques can be adopted to check if UML designs are complete or consistent. A new component called property parser was developed and merged into the tool SAM Parser, which realize (sub)system models automatically. The property parser generates and weaves runtime monitoring code into system implementations automatically for dependability assurance. The framework in the investigation is creative and flexible since it not only can be explored to verify and validate UML designs, but also provides an approach to build models for various scenarios. As a result of my research, several kinds of previous ignored behavioral inconsistencies can be detected.^

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic.^ This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.^

A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net

The purpose of this research was to apply model checking by using a symbolic model checker on Predicate Transition Nets (PrT Nets). A PrT Net is a formal model of information flow which allows system properties to be modeled and analyzed. The aim of this thesis was to use the modeling and analysis power of PrT nets to provide a mechanism for the system model to be verified. Symbolic Model Verifier (SMV) was the model checker chosen in this thesis, and in order to verify the PrT net model of a system, it was translated to SMV input language. A software tool was implemented which translates the PrT Net into SMV language, hence enabling the process of model checking. The system includes two parts: the PrT net editor where the representation of a system can be edited, and the translator which converts the PrT net into an SMV program.

Formal verification and testing of software architectural models

Ensuring the correctness of software has been the major motivation in software research, constituting a Grand Challenge. Due to its impact in the final implementation, one critical aspect of software is its architectural design. By guaranteeing a correct architectural design, major and costly flaws can be caught early on in the development cycle. Software architecture design has received a lot of attention in the past years, with several methods, techniques and tools developed. However, there is still more to be done, such as providing adequate formal analysis of software architectures. On these regards, a framework to ensure system dependability from design to implementation has been developed at FIU (Florida International University). This framework is based on SAM (Software Architecture Model), an ADL (Architecture Description Language), that allows hierarchical compositions of components and connectors, defines an architectural modeling language for the behavior of components and connectors, and provides a specification language for the behavioral properties. The behavioral model of a SAM model is expressed in the form of Petri nets and the properties in first order linear temporal logic. This dissertation presents a formal verification and testing approach to guarantee the correctness of Software Architectures. The Software Architectures studied are expressed in SAM. For the formal verification approach, the technique applied was model checking and the model checker of choice was Spin. As part of the approach, a SAM model is formally translated to a model in the input language of Spin and verified for its correctness with respect to temporal properties. In terms of testing, a testing approach for SAM architectures was defined which includes the evaluation of test cases based on Petri net testing theory to be used in the testing process at the design level. Additionally, the information at the design level is used to derive test cases for the implementation level. Finally, a modeling and analysis tool (SAM tool) was implemented to help support the design and analysis of SAM models. The results show the applicability of the approach to testing and verification of SAM models with the aid of the SAM tool.

Gender, language and floor apportionment in political debates

Political debates are speech events which foreground issues of power and the `floor', and allow the opportunity of assessing the ways in which the gender of participants affects their construction as more or less powerful participants in debates. Debates in the British House of Commons are adversarial in style, making it appropriate to view the floor as `the site of a contest where there is a winner and a loser'. Previous research into political debates has found that male participants violate the formal rules in debates more than their female counterparts, in order to gain the floor. Although the canonical form and rules of debates exist to `permit the equalization of turns', rule violations are common, and inequalities between participants exist. In this article legal and illegal interventions are evaluated in five debates in order to establish the extent to which the gender of participants is related to the control that an individual has over the debate floor.

'I am not an Honourable Lady': gender and language in the National Assembly for Wales

Women have been historically underrepresented in political institutions and it has been claimed that it is difficult for women to succeed in the masculinist cultures that exist in political contexts. The ‘new’ devolved institutions of the UK offer opportunities to investigate gender inequality in political contexts which have a greater proportion of women members; that have included women from their inception; and that have been designed with egalitarian issues to the fore. Here, ethnographic and discourse analytic data is used to assess a senior woman’s performance in the National Assembly for Wales; to explore politicians’ appraisal of this performance; and to analyse the breakdown of the debate floor in terms of ‘rule-breaking’ activities such as barracking. In this Community of Practice the individual’s performance draws upon communicative styles that are both stereotypically masculine (adversarial) and feminine (consensual), which can be viewed as an indication of the speaker’s competence. However, this is undermined by the speaker’s failure to adopt the correct linguistic practices for this CoP which leads to the breakdown of the formal debate discourse. Assembly Members appraise this failure negatively while also drawing upon stereotypical notions of gendered communicative norms and wider discourses of gender differentiation.

Estructura formal, textual y oral del discurso público

Estructura formal, textual y oral del discurso públicoExisten tres competencias comunicativas muy valoradas en la sociedad de la información. Primero, la búsqueda, selección y gestión de grandes cantidades de información. Segundo, la redacción de textos claros, concisos y rigurosos. Y en tercer lugar, la exposición y defensa oral de esta información en un discurso público. Tradicionalmente, los estudios de periodismo han abordado estas competencias de forma independiente. Pero actualmente, instituciones y empresas de ámbitos diferentes demandan un perfil profesional capaz de aplicarlas ante cualquier tipo de información y con objetivos diversos. Se propone un modelo integral en tres niveles estructurales basado en teorías, conceptos y estudios específicos de periodismo, oratoria, retórica… o comunicación, en los últimos años. Este modelo puede contribuir a encauzar las investigaciones de académicos y representa una herramienta de entrenamiento para profesionales.

Formal and informal translation and interpretation for immigrants and asylum seekers

As of 2011 there were over 50,000 migrants, who speak a language other than English or Irish at home, residing in Northern Ireland. Many of these individuals do not possess adequate levels of English language proficiency in order to access services. Research funded by the Northern Ireland Inclusion and Diversity Service was conducted to determine the home-school connections of culturally and linguistically diverse families in Northern Ireland. It revealed that there are a wide variety of ways that translation and interpretation services are offered for families not fluent in English within the school settings. Drawing upon the findings from the research in Northern Ireland, this presentation provides an overview of the types of translation and interpretation taking place in Northern Ireland; the advantages and disadvantages of each; and recommendations for agencies utilizing both formal and informal translation and interpretation. The presentation also includes references to work in this area in other contexts, as well as specific guidelines for agencies using both formal and informal translation and interpretation. These guidelines help ensure that the translations are conducted in a professional manner for all agencies providing services.