Wyniki wyszukiwania - BazTech

1

BioModelKit : Spatial Modelling of Complex Multiscale Molecular Biosystems Based on Modular Models

Blätke M.-A., Rohr C.

Fundamenta Informaticae

|

2018

|

Vol. 160, nr 1/2

221--254

EN

Systems and synthetic biology require multiscale biomodel engineering approaches to integrate diverse spatial and temporal scales which will help to better understand and describe the various interactions in biological systems. Our BioModelKit framework for modular biomodel engineering allows composing multiscale models from a set of modules, each describing an individual biomolecular component in the form of a Petri net. In this framework, we now propose a feature for spatial modelling of molecular biosystems. The spatial model represents the coordinates and movement of individual biomolecular components on a defined grid. Here, the distance between components constrains their ability to interact with each other. We use coloured Petri nets to scale the spatial model, such that each molecular component can exist in an arbitrary number of instances. The grid can encode various regular and irregular structures according to the cellular arrangement and geometry. Furthermore, the grid can be divided into compartments to represent the compartmentalisation of the cell.

2

On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols: Coloured Petri Nets-based Method

Permpoontanalarp Y., Sornkhom P.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 4

423--466

EN

Most Petri nets-based methods that have been developed to analyze cryptographic protocols provide the analysis of one attack trace only. Only a few of them offer the analysis of multiple attack traces, but they are rather inefficient. Analogously, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. In this paper, we propose a very simple but practical Coloured Petri nets-based model checking method for the analysis of cryptographic protocols, which overcomes these limitations. Our method offers an efficient analysis of multiple attack traces. We apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali's contract signing protocol. Surprisingly, our simple method is very efficient when the numbers of attack traces and states are large. Also, we find many new attacks in those protocols.

3

Modelling and Validation of Secure Connection Establishment in a Generic Access Network Scenario

Kristensen L.M., Fleischer P.

Fundamenta Informaticae

|

2009

|

Vol. 94, nr 3/4

361-386

EN

The Generic Access Network (GAN) architecture is defined by the 3rd Generation Partnership Project (3GPP) and allows telephone services, such as SMS and voice-calls, to be accessed via Internet Protocol (IP) networks. The main usage of this is to allow mobile phones to use WiFi in addition to the usual GSM network. The GAN specification relies on the Internet Protocol Security layer (IPSec) and the Internet Key Exchange protocol (IKEv2) to provide encryption across IP networks, and thus avoid compromising the security of the telephone networks. The detailed usage of these two Internet protocols (IPSec and IKEv2) is not fully described in the GAN specification. As part of the process to develop solutions to support the GAN architecture, TietoEnator Denmark has developed a detailed GAN scenario which describes how IPSec and IKEv2 are to be used during the connection establishment procedure. This paper presents an industrial project where Coloured Petri Nets (CPNs) were used to specify and validate the detailed GAN scenario considered by TietoEnator.

4

Coloured Petri Net Modelling of an Evolving Internet Standard: the Datagram Congestion Control Protocol

Billington J., Vanit-Anunchai S.

Fundamenta Informaticae

|

2008

|

Vol. 88, nr 3

357-385

EN

The DatagramCongestion Control Protocol (DCCP) is a new transport protocol standardized by the Internet Engineering Task Force (IETF) in March 2006. This paper discusses the specification of the connectionmanagement and synchronization procedures of DCCP using Coloured Petri Nets (CPNs). After introducing the protocol, we describe how the CPN model evolved as DCCP was being developed. We focus on our experience of incremental enhancement in the hope that this will provide guidance to those attempting to build complex protocol models. In particular, we discuss how the architecture, data structures and specification style of the model evolved as DCCP was developed. We finally recommend a procedure-based style once the standard is stable. The impact of this work on the DCCP standard and our interaction with IETF is also briefly discussed.

5

Mapping of petri net formal model of concurrent system to class model with aspect of polymorphism in object oriented paradigm

Wojciechowski J.

Mikroelektronika i Informatyka : prace naukowe

|

2007

|

Z. nr 7

167-170

EN

Models are developed in meny areas of engineering as means of understending the requirements for a system and assessing the chances of a design. In sofware development process, models range from the graphical representations of data i.e. entity-relationship diagram and functionality i.e. UML to the formal mathematical representation of functional and temporal behavior using Petri nets. Aspect of extracting polymorphism dependency from model towards implementation in OO design is presented in this article.

PL

Celem pracy jest zaproponowanie ścieżki przejścia od modelu formalnego systemu opisanego siecią Petriego do implementacji na szczególnym skupieniu się na ekstrakcji cech obiektowych związanych z cechą polimorfizmu modelu. Autor skupia się na rzutowaniu nie hierarchicznych modeli sieci do modelu klas odpowiadającemu obiektowemu paradygmatowi programowania języka Java. Autor rozszerza model formalny o informację umożliwiajacą dokonanie konwersji do modelu klas uwzględniajac polimorfizm modelu. Cały cykl będzie reprezentowany na przypadkach użycia występujących w modelu.

6

Formalising TCP's Data Transfer Service Language: A Symbolic Automaton and its Properties

Billington J., Han B.

Fundamenta Informaticae

|

2007

|

Vol. 80, nr 1-3

49-74

EN

The TCP/IP protocol suite defines the procedures governing the movement of data within the Internet. A major component of the suite is the Transmission Control Protocol (TCP), which ensures data flows reliably between Internet applications. We use Coloured Petri Nets (CPNs) to model the application's view of the service provided by TCP for the transfer of data. This service depends on the storage capacity available in the Internet. We firstly establish exact expressions for the size of the CPN model's reachability graph (or state space) in terms of the storage capacity. They indicate that both the nodes and arcs of the state space grow exponentially in the storage capacity. Secondly, we derive a symbolic state space which represents an infinite family of state spaces, one for each value of the capacity. We prove that each member of this family is a strongly connected graph and that its associated finite state automaton is deterministic and minimum. Finally, we formulate the TCP data transfer service language for arbitrary capacity, from the symbolic representation of the family of automata. This service language is the yardstick against which the TCP data transfer protocol can be verified with respect to user observable sequences of events.

7

Reconstruction of Concurrent System Models Described by Decomposed Data Tables

Suraj Z., Pancerz K.

Fundamenta Informaticae

|

2006

|

Vol. 71, nr 1

121-137

EN

This paper deals with reconstruction of net models of concurrent systems described by information systems changing in time. Constructed net models have the form of coloured Petri nets. Resulting nets are constructed on the basis of decomposed information systems. In many practical cases, a description of modelled systems changes in time. New knowledge about structures and behaviours of systems appears. When new descriptions appear, the net models should be changed taking into consideration the new knowledge. An approach to reconstruction of net models is here presented. One of many possible cases is considered, i.e., when the new global state of the modelled system appears. The ability to compute reducts and components of a new information system, being a new description of a modelled system, in an efficient way is important for reconstruction. Therefore, some propositions and corollaries useful to compute reducts of a new information system on the basis of reducts of an old information system are given. These propositions and corollaries are the basis to formulate algorithms for computing new reducts and components. Moreover, a way to determine the cost of the reconstruction of a net model is given. The cost of the reconstruction is treated as the cost of adding new functional modules, communication lines or their modifications. The discussed approach to model reconstruction extends and refines that proposed by Z. Suraj in 1998. An example is given in this paper to illustrate the presented idea.

8

Zastosowanie kolorowanych sieci Petriego w projektowaniu systemów czasu rzeczywistego

Samolej S., Trybus B.

Pomiary Automatyka Kontrola

|

2005

|

R. 51, nr 1

11-13

PL

W artykule przedstawiono metodę zastosowania kolorowanych sieci Petriego (sieci CPN) do wytwarzania systemów czasu rzeczywistego. Opis systemu prowadzony jest przy użyciu metodyki SDRTS (Structured Design for Real-Time Systems) i sieci CPN. Ostatecznym rezultatem procesu projektowego jest zbiór hierarchicznych czasowych sieci CPN odpowiadajacych diagramom metodyki SDRTS, umożliwiający symulację i formalną analizę wytwarzanego systemu.

EN

A way of application of coloured Petri nets (CPN) in real-time systems development is presented in the paper. The system is described simultaneously using SDRTS (Structured Design for Real-Time Systems) method and CPN language. The final result of the development process is a set of hierarchical timed coloured Petri nets corresponding to SDRTS diagrams that makes it possible to simultane and formally analyse the system designed.

9

Restriction-Based Concurrent System Design Using the Rough Set Formalism

Suraj Z., Pancerz K.

Fundamenta Informaticae

|

2005

|

Vol. 67, nr 1-3

233-247

EN

Design of concurrent systems under various constraints is an important problem in real-life applications in many domains (for example, automatics, robotics, software engineering) and has earlier been discussed in the literature using different formalisms. In this paper some approaches to the concurrent system design based on restrictions will be considered. In our approaches, we will use the rough set formalism. The coloured Petri nets (CP-nets) will be used to model designed concurrent systems.

10

Discovery of Asynchronous Concurrent Models from Experimental Tables

Pancerz K., Suraj Z.

Fundamenta Informaticae

|

2004

|

Vol. 61, nr 2

97--116

EN

The synthesis problem of concurrent systems has earlier been discussed in the literature using different types of formalisms. This paper presents a new method for discovery of asynchronous concurrent models from experimental tables by using a rough set approach. The proposed method can be applied to the automatic data model discovery. The algorithm for constructing asynchronous concurrent models is described in detail. As a model for concurrency the Coloured Petri Nets are used. Constructed asynchronous models can be helpful to solving some problems arising in design of asynchronous digital systems or addressing of nodes in parallel systems. An example illustrates an application of the proposed approach in such problems.

11

Discovering Concurrent Models from Data Tables with the ROSECON System

Pancerz K., Suraj Z.

Fundamenta Informaticae

|

2004

|

Vol. 60, nr 1-4

251--268

EN

This paper presents an approach to discovering concurrent models from data tables using the ROSECON software system. The acronym ROSECON comes from "ROugh SEts and CONcurrency". The models created using ROSECON have the form of Coloured Petri Nets. The ROSECON system is based on the rough set theory. The models derived by ROSECON can be used to determine different properties concerning structures and behaviours of systems. Running examples illustrate some directions one might take in the study of behavioural patterns in information system tables.

12

Synthesis of Petri Net Models: A Rough Set Approach

Pancerz K., Suraj Z.

Fundamenta Informaticae

|

2003

|

Vol. 55, nr 2

149-165

EN

The synthesis problem of concurrent data models from experimental tables based on rough set approach has earlier been discussed [14], [15]. Classical Petri nets have been used as a model for concurrency. In this paper we propose the nets with inhibitor expressions and Coloured Petri Nets as models for concurrency. The nets with inhibitor expressions are defined on the base of so called inhibitor rules extracted from modelled systems. The approach presented in this paper enables to implement the algorithms for easier construction of Petri net models. The proposed approach can be applied to discover data models in semi-automatic way. The obtained models enable us to determine all global states of a modelled system represented by an information system, consistent with all rules extracted from the given information system.

13

Precyzyjna reprezentacja wiedzy niepelnej - zbiory rozmyte i przybliżone

Szmuc T.

Geoinformatica Polonica

|

2002

|

T. 4

55-79

PL

Artykuł zawiera przegląd podstawowych pojęć i metod dotyczących dwóch najbardziej znanych podejść do reprezentacji wiedzy niepełnej: zbiorów rozmytych i zbiorów przybliżonych. Pierwsze z nich bazuje na rozszerzeniu funkcji przynależności na przedział [0, 1], natomiast drugie opisuje niedokładność klasyfikacji przez relację równoważności, tzn. elementy nierozróżnialne należą do tych samych klas. Obie teorie, wywodzące się z dążenia do opisu tego samego problemu przyjmują jednak odrębne założenia początkowe, co oczywiście prowadzi do różnych metod analizy i odmiennych obszarów efektywnego zastosowania. Nie oznacza to jednak całkowitej rozłączności tych obszarów, należy również wspomnieć o możliwości komplementarnego stosowania obu podejść. W opracowaniu nieco mniej miejsca poświęcono zagadnieniom zbiorów rozmytych, gdyż teoria jest szerzej znana, natomiast zbiory przybliżone są podejściem młodszym i słabiej rozpowszechnionym. Efektywność metod oferowanych przez tę teorię jest bardzo dobrze widoczna dla tablicowej reprezentacji wiedzy (tablice decyzyjne). Ten sposób reprezentacji wiedzy jest szeroko stosowany w informatyce (systemy regułowe, wspomaganie podejmowania decyzji, analiza danych, klasyfikacja), co przenosi się na szeroki obszar zastosowań. W końcowej części pracy pokazano alternatywny sposób reprezentacji wiedzy - zastosowanie kolorowanych sieci Petriego. Stanowi to nie tylko alternatywne podejście, lecz również umożliwia rozszerzenie klasy analizowanych tablic, m.in. przez możliwości hierarchizacji.

EN

The paper contains an overview of basic notions and methods related to two mostly known approaches to representation of uncertain knowledge, i.e. fuzzy sets and rough sets. The first approach is based on an extension of membership function into interval [0, 1], while the second one describes uncertainty of classification by equivalence relation, i.e. indistinguishable elements belong to the same classes. The both theories starting from the same requirements related to description ofthe same problem, are based on different assumptions, which lead to different analysis methods and different areas of efficient applications. However, the application areas are not totally disjoint, many examples of complement applications of both methods also can be encountered. Presentation of fuzzy sets theory is relatively less detailed, because the theory is widely known. Rough sets theory is relatively younger and not so popular. Efficiency of methods provided by the theory is especially visible in the case of table knowledge representation (decision tables). This knowledge representation is widely used in computer science (rule-based systems, decision support, data analysis, classification). The wide diversity of the applications implies wide range of areas, where the theory can be applied. In the final part of the paper, an alternative way for knowledge representation is shown. This part describes an application of Coloured Petri nets for specification and analysis of decision tables. It is not only an alternative approach, but also provides possibilities for extensions of class of analysed tables, among others by providing hierarchical structure.