Wyniki wyszukiwania - BazTech

1

Formalization of software risk assessment results in legal metrology based on ISO/IEC 18045 vulnerability analysis

Esche Marko, Salwiczek Felix, Grasso Toro Federico

Annals of Computer Science and Information Systems

|

2019

|

Vol. 18

443--447

EN

The Measuring Instruments Directive sets down essential requirements for measuring instruments subject to legal control in the EU. It dictates that a risk assessment must be performed before such instruments are put on the market. Because of the increasing importance of software in measuring instruments, a specifically tailored software risk assessment method has been previously developed and published. Related research has been done on graphical representation of threats by attack probability trees. The final stage is to formalize the method to prove its reproducibility and resilience against the complexity of future instruments. To this end, an inter-institutional comparison of the method is currently being conducted across national metrology institutes, while the weighing equipment manufacturers' association CECIP has provided a new measuring instrument concept, as a significant example of complex instruments. Based on the results of the comparison, a template to formalize the software risk assessment method is proposed here.

2

Program Verification using Constraint Handling Rules and Array Constraint Generalizations

De Angelis E., Fioravanti F., Pettorossi A., Proietti M.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 1

73--117

EN

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

3

Walidacja programu PLC z wykorzystaniem wirtualnego modelu urządzenia w programie Delmia automation

Słota A., Borowy Sz.

Mechanik

|

2013

|

R. 86, nr 2CD

PL

W pracy przedstawiono tok postepowania przy weryfikacji programu sterownika PLC z wykorzystaniem wirtualnego modelu urządzenia sterowanego w systemie DELMIA. Zadanie zostało zrealizowane dla podajnika palet stacji załadowczo-rozładowczej systemu TOR, sterowanego przez sterownik PLC S7-300. Omówiono budowe wirtualnego modelu urządzenia (Smart Device), definicje modelu panelu operatora, konfiguracje serwera OPC oraz integracje komponentów środowiska. Walidacje programu PLC zrealizowano z wykorzystaniem rzeczywistego sterownika, podłączonego do systemu Delmia za pośrednictwem serwera OPC KEPServerEX.

EN

In the paper a procedure of PLC program validation with the use of a virtual model of controlled device built in Delmia system is presented. The task was realized for pallet changer of loading-unloading station of TOR system controlled by S7-300 PLC controller. Creation of a virtual model of the device (Smart Device), definition of an operator panel model, server OPC configuration and integration of environment components are described. PLC program validation was realized with the use of a real PLC controller connected to Delmia system via OPC server KEPSeverEX.

4

Wirtualny kontroler pionowego centrum obróbkowego FV 580A - symulacja, weryfikacja i analiza porównawcza procesu obróbki

Józwik J., Włodarczyk M., Ścierka T.

Postępy Nauki i Techniki

|

2010

|

nr 5

97-113

PL

W pracy przedstawiono proces generowania wirtualnego kontrolera VNC w aplikacji Post Builder systemu NX z uwzględnieniem typu sterowania maszyny. Skonfigurowano wykonany model kinematyczny wraz z kontrolerem i postprocesorem w bibliotece systemu NX. Przygotowano do obróbki przykładowe modele przy wykorzystaniu Synchronous Technology oraz wykonano program obróbki. Przeprowadzono weryfikację ścieżek i symulację obróbki. W końcowej części pracy porównano zasymulowaną obróbkę z rzeczywistym procesem frezowania podczas prób na maszynie.

EN

In this paper generating process of virtual controller is presented. This process is care out with used NX system with Post Builder application and take into type of steering machine system. Kinematics model with controller and postprocessor in NX library was configured. Machining process of geometrical models with used Synchronous Technology and NC program was developed. In this article tool path verification and simulation is presented. Finally, process of machining simulation and real cutting process during tests on CNC machine tool is compared.

5

Nets with Tokens which Carry Data

Lazić R., Newcomb T., Ouaknine J., Roscoe A.W., Worrell J.

Fundamenta Informaticae

|

2008

|

Vol. 88, nr 3

251-274

EN

We study data nets, a generalisation of Petri nets in which tokens carry data from linearlyordered infinite domains and in which whole-place operations such as resets and transfers are possible. Data nets subsume several known classes of infinite-state systems, including multiset rewriting systems and polymorphic systems with arrays. We show that coverability and termination are decidable for arbitrary data nets, and that boundedness is decidable for data nets in which whole-place operations are restricted to transfers. By providing an encoding of lossy channel systems into data nets without whole-place operations, we establish that coverability, termination and boundedness for the latter class have non-primitive recursive complexity. The main result of the paper is that, even for unordered data domains (i.e., with only the equality predicate), each of the three verification problems for data nets without whole-place operations has non-elementary complexity.