Wyniki wyszukiwania - BazTech

1

Research on reliability of mobile applications in a distributed environment

Ławrynowicz Mirosław, Legut Jakub, Jóźwiak Ireneusz J.

Zeszyty Naukowe. Organizacja i Zarządzanie / Politechnika Śląska

|

2020

|

z. 144

327--337

EN

Purpose: The purpose of the paper is to present the research on reliability of mobile applications in distributed systems. Design/methodology/approach: Ensuring the reliable operation of the software created for Android OS is related to ensuring compatibility with different versions of the systems. The use of various security policies, formal and structural requirements in various Android releases results in a high failure rate of dedicated programs. Findings: There is, therefore, a need to implement new testing methods. Originality/value: The article proposes a method of software reliability analysis dedicated to distributed systems. The developed solution is based on concurrency using the actor model. As part of the research, the effectiveness of the developed solutions was evaluated.

2

A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell

Albert Elvira, Bezirgiannis Nikolaos, de Boer Frank, Martin-Martin Enrique

Fundamenta Informaticae

|

2020

|

Vol. 177, nr 3/4

203--234

EN

We present a formal translation of a resource-aware extension of the Abstract Behavioral Specification (ABS) language to the functional language Haskell. ABS is an actor-based language tailored to the modeling of distributed systems. It combines asynchronous method calls with a suspend and resume mode of execution of the method invocations. To cater for the resulting cooperative scheduling of the method invocations of an actor, the translation exploits for the compilation of ABS methods Haskell functions with continuations. The main result of this article is a correctness proof of the translation by means of a simulation relation between a formal semantics of the source language and a high-level operational semantics of the target language, i.e., a subset of Haskell. We further prove that the resource consumption of an ABS program extended with a cost model is preserved over this translation, as we establish an equivalence of the cost of executing the ABS program and its corresponding Haskell-translation. Concretely, the resources consumed by the original ABS program and those consumed by the Haskell program are the same, considering a cost model. Consequently, the resource bounds automatically inferred for ABS programs extended with a cost model, using resource analysis tools, are sound resource bounds also for the translated Haskell programs. Our experimental evaluation confirms the resource preservation over a set of benchmarks featuring different asymptotic costs.

3

Active resources concept of computation for enterprise software

Koryl M.

Archives of Control Sciences

|

2017

|

Vol. 27, no. 2

279--291

EN

Traditional computational models for enterprise software are still to a great extent centralized. However, rapid growing of modern computation techniques and frameworks causes that contemporary software becomes more and more distributed. Towards development of new complete and coherent solution for distributed enterprise software construction, synthesis of three well-grounded concepts is proposed: Domain-Driven Design technique of software engineering, REST architectural style and actor model of computation. As a result new resources-based framework arises, which after first cases of use seems to be useful and worthy of further research.

4

Regularising Ill-posed Discrete Optimisation: Quests with P Systems

Nicolescu R., Gimel’farb G., Morris J., Delmas P., Gong R.

Fundamenta Informaticae

|

2014

|

Vol. 131, nr 3-4

465--483

EN

We propose a novel approach to justify and guide regularisation of an ill-posed one-dimensional global optimisation with multiple solutions using a massively parallel (P system) model of the solution space. Classical optimisation assumes a well-posed problem with a stable unique solution. Most of important practical problems are ill posed due to an unstable or non-unique global optimum and are regularised to get a unique best-suited solution. Whilst regularisation theory exists largely for unstable unique solutions, its recommendations are often routinely applied to inverse optical problems with essentially non-unique solutions, e.g. computer stereo vision or image segmentation, typically formulated in terms of global energy minimisation. In these cases the recommended regularisation becomes purely heuristic and does not guarantee a unique solution. As a result, classical optimisation algorithms: dynamic programming (DP) and belief propagation (BP) – meet with difficulties. Our recent concurrent propagation (CP), leaning upon the P systems paradigm, extends DP and BP to always detect whether the problem is ill posed or not and store in the ill-posed case an entire space of solutions that yield the same global optimum. This suggests a radically new path to proper regularisation: select the best-suited unique solution by exploring statistical and structural features of this space. We propose a P systems based implementation of CP and set out as a case study an application of CP to the image matching problem in stereo vision.

5

Modeling and Verification of Reactive Systems using Rebeca

Sirjani M., Movaghar A., Shali A., de Boer F. S.

Fundamenta Informaticae

|

2004

|

Vol. 63, nr 4

385--410

EN

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their correctness. In this paper, we develop an actor-based model for describing such systems, use temporal logic to specify properties of the model, and apply different abstraction and verification methods for verifying that the model meets its specification. We use a compositional verification approach for verifying safety properties of these models. For that we introduce a notion of component, based on an user-defined decomposition of the model. Components are more abstract than the model itself, and so we can reduce the state space of the model which makes it more amenable to model checking techniques. We prove that our abstraction technique preserves a set of behavioral specifications in temporal logic. The soundness of the abstraction is proved by the weak simulation relation between the constructs.