An automated tool for semantic accessing to formal software models

Many software engineers have found that it is difficult to understand, incorporate and use different formal models consistently in the process of software developments, especially for large and complex software systems. This is mainly due to the complex mathematical nature of the formal methods and the lack of tool support. It is highly desirable to have software models and their related software artefacts systematically connected and used collaboratively, rather than in isolation. The success of the Semantic Web, as the next generation of Web technology, can have profound impact on the environment for formal software development. It allows both the software engineers and machines to understand the content of formal models and supports more effective software design in terms of understanding, sharing and reusing in a distributed manner. To realise the full potential of the Semantic Web in formal software development, effectively creating proper semantic metadata for formal software models and their related software artefacts is crucial. This paper proposed a framework that allows users to interconnect the knowledge about formal software models and other related documents using the semantic technology. We first propose a methodology with tool support is proposed to automatically derive ontological metadata from formal software models and semantically describe them. We then develop a Semantic Web environment for representing and sharing formal Z/OZ models. A method with prototype tool is presented to enhance semantic query to software models and other artefacts. © 2014.

Formal Definition of Artificial Intelligence

* This publication is partially supported by the KT-DigiCult-Bg project.

Formal Definition of the Concept “Infos”

The concept INFOS is very important for understanding the information phenomena. Because of this, it is basic for the General Information Theory. The more precise formal definition of this concept is given in the paper.

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.

Computer-Assisted Proofs and Symbolic Computations

We discuss some main points of computer-assisted proofs based on reliable numerical computations. Such so-called self-validating numerical methods in combination with exact symbolic manipulations result in very powerful mathematical software tools. These tools allow proving mathematical statements (existence of a fixed point, of a solution of an ODE, of a zero of a continuous function, of a global minimum within a given range, etc.) using a digital computer. To validate the assertions of the underlying theorems fast finite precision arithmetic is used. The results are absolutely rigorous. To demonstrate the power of reliable symbolic-numeric computations we investigate in some details the verification of very long periodic orbits of chaotic dynamical systems. The verification is done directly in Maple, e.g. using the Maple Power Tool intpakX or, more efficiently, using the C++ class library C-XSC.

Symmetric and Asymmetric Gaps in Some Fields of Formal Power Series

2000 Mathematics Subject Classification: 03E04, 12J15, 12J25.

Formal Specification of Relational Model of Data in Z-Notation

Владимир Димитров - Целта на настоящия доклад е формалната спецификация на релационния модел на данни. Тази спецификация след това може да бъде разширена към Обектно-релационния модел на данни и към Потоците от данни.

Verification of Procedural Programs via Building their Generalized Nets Models

Магдалина Василева Тодорова - В статията е описан подход за верификация на процедурни програми чрез изграждане на техни модели, дефинирани чрез обобщени мрежи. Подходът интегрира концепцията “design by contract” с подходи за верификация от тип доказателство на теореми и проверка на съгласуваност на модели. За целта разделно се верифицират функциите, които изграждат програмата относно спецификации според предназначението им. Изгражда се обобщен мрежов модел, специфициащ връзките между функциите във вид на коректни редици от извиквания. За главната функция на програмата се построява обобщен мрежов модел и се проверява дали той съответства на мрежовия модел на връзките между функциите на програмата. Всяка от функциите на програмата, която използва други функции се верифицира и относно спецификацията, зададена чрез мрежовия модел на връзките между функциите на програмата.

Social - Oriented Applications of the Folklore Heritage for the Needs of the Non-formal Learning and Cultural Tourisms

The report presents a description of the most popular digital folklore archives in the world. Specifications for designing and developing web-based social-oriented applications in the field of education and cultural tourism are formulated on the basis of comparative analysis. A project for structuring and categorizing the content is presented. A website for accessing the digital folklore archive is designed and implemented.

Formal methods @ runtime

Heuristics, simulation, artificial intelligence techniques and combinations thereof have all been employed in the attempt to make computer systems adaptive, context-aware, reconfigurable and self-managing. This paper complements such efforts by exploring the possibility to achieve runtime adaptiveness using mathematically-based techniques from the area of formal methods. It is argued that formal methods @ runtime represents a feasible approach, and promising preliminary results are summarised to support this viewpoint. The survey of existing approaches to employing formal methods at runtime is accompanied by a discussion of their challenges and of the future research required to overcome them. © 2011 Springer-Verlag.

Formal methods for the development and verification of autonomic IT systems

This chapter explores ways in which rigorous mathematical techniques, termed formal methods, can be employed to improve the predictability and dependability of autonomic computing. Model checking, formal specification, and quantitative verification are presented in the contexts of conflict detection in autonomic computing policies, and of implementation of goal and utility-function policies in autonomic IT systems, respectively. Each of these techniques is illustrated using a detailed case study, and analysed to establish its merits and limitations. The analysis is then used as a basis for discussing the challenges and opportunities of this endeavour to transition the development of autonomic IT systems from the current practice of using ad-hoc methods and heuristic towards a more principled approach. © 2012, IGI Global.

The Shapley value for airport and irrigation games

In this paper cost sharing problems are considered. We focus on problems given by rooted trees, we call these problems cost-tree problems, and on the induced transferable utility cooperative games, called irrigation games. A formal notion of irrigation games is introduced, and the characterization of the class of these games is provided. The well-known class of airport games Littlechild and Thompson (1977) is a subclass of irrigation games. The Shapley value Shapley (1953) is probably the most popular solution concept for transferable utility cooperative games. Dubey (1982) and Moulin and Shenker (1992) show respectively, that Shapley's Shapley (1953) and Young (1985)'s axiomatizations of the Shapley value are valid on the class of airport games. In this paper we show that Dubey (1982)'s and Moulin and Shenker (1992)'s results can be proved by applying Shapley (1953)'s and Young (1985)'s proofs, that is those results are direct consequences of Shapley (1953)'s and Young (1985)'s results. Furthermore, we extend Dubey (1982)'s and Moulin and Shenker (1992)'s results to the class of irrigation games, that is we provide two characterizations of the Shapley value for cost sharing problems given by rooted trees. We also note that for irrigation games the Shapley value is always stable, that is it is always in the core Gillies (1959).

Formal professional relationships between general practitioners and specialists: possible associations with patient health and pharmacy costs

This article investigates whether the strength of formal professional relationships between general practitioners (GPs) and specialists (SPs) affects either the health status of patients or their pharmacy costs. To this end, it measures the strength of formal professional relationships between GPs and SPs through the number of shared patients and proxies the patient health status by the number of comorbidities diagnosed and treated. In strong GP–SP relationships, the patient health status is expected to be high, due to efficient care coordination, and the pharmacy costs low, due to effective use of resources. To test these hypotheses and compare the characteristics of the strongest GP–SP connections with those of the weakest, this article concentrates on diabetes—a chronic condition where patient care coordination is likely important. Diabetes generates the largest shared patient cohort in Hungary, with the highest traffic of specialist medication prescriptions. This article finds that stronger ties result in lower pharmacy costs, but not in higher patient health statuses. Key points for decision makers • The number of shared patients may be used to measure the strength of formal professional relationships between general practitioners and specialists. • A large number of shared patients indicates a strong, collaborative tie between general practitioners and specialists, whereas a low number indicates a weak, fragmented tie. • Tie strength does not affect patient health—strong, collaborative ties between general practitioners and specialists do not involve better patient health than weak, fragmented ties. • Tie strength does affect pharmacy costs—strong, collaborative ties between general practitioners and specialists involve significantly lower pharmacy costs than weak, fragmented ties. • Pharmacy costs may be reduced by lowering patient care fragmentation through channelling a general practitioner’s patients to a small number of specialists and increasing collaboration between general practitioner and specialists. • Limited patient choice is financially more beneficial than complete freedom of choice, and no more detrimental to patient health.

A gyógyszerkiadás és a betegek egészségi állapota a háziorvosi és szakorvosi kapcsolatok függvényében = Formal professional relations between general practitioners and specialists. Possible links with patient health and pharmacy cost

Arra a kérdésre keressük a választ, hogy a szoros háziorvosi-szakorvosi szakmai kapcsolatoknak van-e hatásuk a betegek gyógyszerkiadására, illetve egészségi állapotára. Az orvosok közötti szakmai kapcsolatok szorosságát a közösen gondozott betegek száma alapján határoztuk meg, míg a betegek egészségügyi állapotát a diagnosztizált és kezelt társbetegségek számával mértük. Hipotézisünk egyrészt az volt, hogy a hatékonyabb koordinációnak köszönhetően a szoros kapcsolatban kezelt betegek jobb egészségi állapotúak, másrészt kezelésük az erőforrások hatékonyabb felhasználása miatt kisebb gyógyszerköltséggel jár. E két hipotézist a cukorbetegekre teszteltük. Azért esett erre a krónikus betegségre a választásunk, mert itt a háziorvosok és a szakorvosok együttműködése elsődleges fontosságú. Magyarországon a cukorbetegek esetében a legnagyobb a közösen kezelt betegek populációja, valamint itt a legmagasabb a szakorvosi javaslatra felírt háziorvosi receptek száma. Azt az eredményt kaptuk, hogy a szoros kapcsolatban kezelt betegek nem rendelkeznek sem jobb, sem rosszabb egészségi állapottal, miközben a kapcsolódó gyógyszerkiadásuk szignifikánsan alacsonyabb. ____ The article considers whether strong formal professional relations between GPs and specialists in shared care affect either the health of patients or the pharmacy costs they incur. The strength of such relations is measured by the number of shared patients; patient health is proxied by number of co-morbidities diagnosed and treated. The first hypothesis is that patients treated amid strong GP-specialist relations have better health status than those treated amid weak ones, due to enhanced efficiency of care coordination. The second is that patients treated in such strong relations incur lower pharmacy costs high numbers of shared patients are assumed to promote appropriate, effective use of resources. The article tests these hypotheses and compares the outcomes of the strongest and weakest GP-specialist relations through the example of diabetes, a chronic condition where patient-care coordination is important. Diabetes generates the largest shared patient cohort in Hungary, with the highest number of specialist medication prescriptions. This article finds that stronger ties result in significantly lower pharmacy costs, but not a higher patient health status.