Wyniki wyszukiwania - BazTech

1

Jak zapewnić poprawności działania programów komputerowych?

Greniewski M. J.

Studia i Materiały / Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie

|

2015

|

Nr 2(10)

1--15

PL

Narasta problem skutków błędów w oprogramowaniu. Konieczna stała się zmiana podejścia – zapewnienie poprawności działania programów komputerowych. Dotyczy to głównie programów współbienych – reaktywnych. Metody formalne pozwalają na zastąpienie metody testowania programów (o wątpliwej skuteczności) metodami walidacji, czyli dowodzenia poprawności działania przez sprawdzanie stanów osiagąnych przez model sterowania programu. Podstawą jest pomysł użycia logiki temporalnej do opisu działania programów współbiernych Amira Pnueli z 1977 roku, który został rozwinięty na początku lat osiemdziesiątych ubiegłego wieku w teorie przez Clarke’a, Emersona oraz Sifakisa (uhonorowani w 2007 r. ACM A.M. Turing Award). Wzmiankowana teorie zastosowano w języku modelowania Promela oraz procesorze Spin (Simple Promela Interpreter) autorstwa zespołu Gerarda J. Holzmanna (uhonorowanego w 2002 r. ACM Software System Award).

EN

There is a growing tendency of the effects of bugs in the software. It becomes necessary to change the approach – to ensure proper operation of computer programs. This applies mainly to concurrent programs – reactive ones. Formal methods allow substitution of the method of testing programs (of dubious efficacy) by validation methods, which is proving the correctness of the action – by checking the status achieved by the control model program. The basis is the idea of using temporal logic to describe the actions of concurrent programs by Amir Pnueli from 1977, further developed in the early eighties of the last century into the theory of Clarke, Emerson and Sifakis (honored in 2007 ACM A.M. Turing Award). The theory mentioned above, was used in modeling language Promela and Spin processor (Simple Promela Interpreter) by Gerard J. Holzmann team (which won the 2002 ACM Software System Award).

2

Logistics systems maintenance modelling problems - the use of TDA approach

Werbińska-Wojciechowska S.

Logistics and Transport

|

2012

|

Vol. 15, No. 2

63-74

EN

The article presents an overview of some recent developments in the area of mathematical modelling of maintenance decisions with the use of time-delay and time-delay analysis. Thus, the literature overview in the investigated area is provided. The problem of time relations occurred in supply chain performance process is investigated. Later, there are presented obtained reliability analysis results in comparison with the knowledge about the case company present condition. The article investigates the possibilities of basic time delay model implementation in the area of logistic system of sixteen forklifts performance analysis.

3

Gaps in design and tests of dependable embedded systems

Grobelna I., Grobelny M.

Metody Informatyki Stosowanej

|

2010

|

nr 2 (23)

45-51

EN

The paper focuses on gaps in design and test technology for dependable embedded systems. Possible gaps in design may influence system behavior and as the result final product may not fulfill all requirements or some of desired properties. Test phase is also important as it may indicate even subtle errors which occurred in previous phases. The article presents possible solutions to improve the design and test technology. Model checking technique can be used for formal verification of specification in design phase. Testing phase can involve independent tester teams.

4

Two-Dimensional Automatic Control Modeling of a Posture Control System

Park K. S., Kim U. H.

International Journal of Occupational Safety and Ergonomics

|

1998

|

Vol. 4, No. 4

485--498

EN

A posture control model has been developed on the basis of the 2-dimensional feedback control theory. Human postural characteristics were investigated in 5 healthy participants. Tests were performed with eyes open and eyes closed. After 5 s of quiet standing, each participant was unexpectedly pulled forward by 30 mm at his pelvis height and then released. Postural sway was measured over 20 s at a rate of 100 per second. Transfer functions to represent the posture control characteristic were identified by the least squares' method. These showed good results of the model's fitness, predictability, and stability. The response of the eyes-closed condition to perturbation is more oscillatory than that of the eyes-open condition. It seems that the model identified could be applicable to ergonomics, sports, or clinical situations.