Automatic Translation of MSC Diagrams into Petri Nets

Development-engineers use in their work languages intended for software or hardware systems design, and test engineers utilize languages effective in verification, analysis of the systems properties and testing. Automatic interfaces between languages of these kinds are necessary in order to avoid ambiguous understanding of specification of models of the systems and inconsistencies in the initial requirements for the systems development. Algorithm of automatic translation of MSC (Message Sequence Chart) diagrams compliant with MSC’2000 standard into Petri Nets is suggested in this paper. Each input MSC diagram is translated into Petri Net (PN), obtained PNs are sequentially composed in order to synthesize a whole system in one final combined PN. The principle of such composition is defined through the basic element of MSC language — conditions. While translating reference table is developed for maintenance of consistent coordination between the input system’s descriptions in MSC language and in PN format. This table is necessary to present the results of analysis and verification on PN in suitable for the development-engineer format of MSC diagrams. The proof of algorithm correctness is based on the use of process algebra ACP. The most significant feature of the given algorithm is the way of handling of conditions. The direction for future work is the development of integral, partially or completely automated technological process, which will allow designing system, testing and verifying its various properties in the one frame.

Extended Algorithm for Translation of MSC-diagrams into Petri Nets

The article presents an algorithm for translation the system, described by MSC document into Petri Net modulo strong bisimulation. Obtained net can be later used for determining various systems' properties. Example of correction error in original system with using if described algorithm presented.

A nested Petri net framework for modeling and analyzing multi-agent systems

In the past two decades, multi-agent systems (MAS) have emerged as a new paradigm for conceptualizing large and complex distributed software systems. A multi-agent system view provides a natural abstraction for both the structure and the behavior of modern-day software systems. Although there were many conceptual frameworks for using multi-agent systems, there was no well established and widely accepted method for modeling multi-agent systems. This dissertation research addressed the representation and analysis of multi-agent systems based on model-oriented formal methods. The objective was to provide a systematic approach for studying MAS at an early stage of system development to ensure the quality of design. ^ Given that there was no well-defined formal model directly supporting agent-oriented modeling, this study was centered on three main topics: (1) adapting a well-known formal model, predicate transition nets (PrT nets), to support MAS modeling; (2) formulating a modeling methodology to ease the construction of formal MAS models; and (3) developing a technique to support machine analysis of formal MAS models using model checking technology. PrT nets were extended to include the notions of dynamic structure, agent communication and coordination to support agent-oriented modeling. An aspect-oriented technique was developed to address the modularity of agent models and compositionality of incremental analysis. A set of translation rules were defined to systematically translate formal MAS models to concrete models that can be verified through the model checker SPIN (Simple Promela Interpreter). ^ This dissertation presents the framework developed for modeling and analyzing MAS, including a well-defined process model based on nested PrT nets, and a comprehensive methodology to guide the construction and analysis of formal MAS models.^

Formal modeling and analysis techniques for high level Petri nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. ^ There are two issues in using HLPNs—modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. ^ For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. ^ For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. ^ The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.^

Formal Modeling and Analysis Techniques for High Level Petri Nets

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Petri Net Siphon Analysis and Network Centrality Measures for Identifying Combination Therapies in Signaling Pathways

Aberrant behavior of biological signaling pathways has been implicated in diseases such as cancers. Therapies have been developed to target proteins in these networks in the hope of curing the illness or bringing about remission. However, identifying targets for drug inhibition that exhibit good therapeutic index has proven to be challenging since signaling pathways have a large number of components and many interconnections such as feedback, crosstalk, and divergence. Unfortunately, some characteristics of these pathways such as redundancy, feedback, and drug resistance reduce the efficacy of single drug target therapy and necessitate the employment of more than one drug to target multiple nodes in the system. However, choosing multiple targets with high therapeutic index poses more challenges since the combinatorial search space could be huge. To cope with the complexity of these systems, computational tools such as ordinary differential equations have been used to successfully model some of these pathways. Regrettably, for building these models, experimentally-measured initial concentrations of the components and rates of reactions are needed which are difficult to obtain, and in very large networks, they may not be available at the moment. Fortunately, there exist other modeling tools, though not as powerful as ordinary differential equations, which do not need the rates and initial conditions to model signaling pathways. Petri net and graph theory are among these tools. In this thesis, we introduce a methodology based on Petri net siphon analysis and graph network centrality measures for identifying prospective targets for single and multiple drug therapies. In this methodology, first, potential targets are identified in the Petri net model of a signaling pathway using siphon analysis. Then, the graph-theoretic centrality measures are employed to prioritize the candidate targets. Also, an algorithm is developed to check whether the candidate targets are able to disable the intended outputs in the graph model of the system or not. We implement structural and dynamical models of ErbB1-Ras-MAPK pathways and use them to assess and evaluate this methodology. The identified drug-targets, single and multiple, correspond to clinically relevant drugs. Overall, the results suggest that this methodology, using siphons and centrality measures, shows promise in identifying and ranking drugs. Since this methodology only uses the structural information of the signaling pathways and does not need initial conditions and dynamical rates, it can be utilized in larger networks.

Das (exemte) Bistum Meißen 1. Das Kollegiatstift St. Petri zu Bautzen von der Gründung bis 1569

Die Arbeit behandelt das Kollegiatstift St. Petri zu Bautzen von dessen Gründung vor 1221 bis zum Jahr 1569. Neben der Gründungsphase des Stiftes und damit einhergehender Fragen zum Verhältnis geistlicher und weltlicher Mächte in der Oberlausitz werden nach dem bewährten Gliederungsschema der Germania Sacra das geistige Leben, die Verfassung und die Stiftswirtschaft vorgestellt. Nach dem Domstift Meißen stellte St. Petri in Bautzen die wichtigste Einrichtung des Bistums dar. Die 1569 dem Bautzener Kapitel übertragene geistliche Administratur auf römisch-katholische Teile der Oberlausitz sicherte dem Stift den Fortbestand bis in die Gegenwart und zugleich die geschlossene Erhaltung seines Urkunden- und Aktenbesitzes. Der schriftlichen Überlieferung lassen sich detaillierte Informationen zum Stiftungswesen, dem Verhältnis zur Stadt, zum Landesherrn und zu anderen geistlichen Einrichtungen entnehmen. Nicht zuletzt dem Weiterbestehen des Bautzener Kollegiatstiftes unter Dekan Johannes Leisentritt verdankt die Oberlausitz ihre besondere Stellung als bikonfessionelles Nebenland der böhmischen Krone. Ein umfangreicher Besitzkatalog und die Viten der Dignitäre und Kanoniker bieten eine breite Materialbasis auch für weitergehende Fragestellungen.

From Hardware Processes to asynchronous circuits via petri nets: An Application to Arbiter Design

International audience

Effata et oracula Montanistarum : programma, quo inaugurationem reverendissimi episcopi Arhusiensis, Petri Johannis Mønster ... secundo natalitiorum Christi die festo in æde divæ virginis solemni ritu peragendam /

Includes bibliographical references.

Determinization of timed Petri nets behaviors

International audience

Prevalence of mutans streptococci isolated from complete dentures and their susceptibility to mouthrinses

The aims of this study were to evaluate the incidence of mutans streptococci (MS - sessile form) on complete maxillary dentures after use of a specific denture paste, and to determine the minimum inhibitory concentration (MIC) and maximum inhibitory dilution (MID) of 3 oral mouthrinses: Cepacol, Plax and Periogard. Seventy-seven complete denture wearers were randomly assigned into 2 groups, according to the product used for denture cleaning: Control group - conventional dentifrice (Kolynos-Super White); and Test group: experimental denture cleaning paste. Denture biofilm was collected at baseline and after 90 and 180 days after treatment by brushing the dentures with saline solution. After decimal serial dilution, samples were seeded onto agar sucrose bacitracin to count colonies with morphological characteristics of MS. MS identification was performed by the sugar fermentation tests. After this procedure, brain heart infusion broth (BHI) was added to oral mouthrinses (Plax, Cepacol e Periogard) and seeded on Petri dishes. The colonies were seeded using the Steers multiplier and, after the incubation, the MIC and MID of the mouthrinses were calculated. The results showed an incidence of 74.0% (n=57) of MS in the 77 complete dentures examined in the study, being 76.3% (n=29) of the Control group (conventional dentifrice) and 71.8% (28) of the Test group (experimental denture cleaning paste). In both groups, the number of positive cases for MS decreased from day 0 to day 180. In the Test group there was a slight decrease in the incidence of Streptococcus mutans 90 days after use of the experimental denture cleaning paste, which was not observed in the Control group. As regards to mouthrinses, for both groups, Periogard showed antimicrobial action with the highest dilution, followed by Cepacol and Plax. In conclusion, the incidence of MS in complete dentures was high and Periogard was the mouthrinse with the strongest antimicrobial action against MS. The experimental denture cleaning paste showed a slight action against S. mutans after 90 days of treatment.

Maximum inhibitory dilution of mouthwashes containing chlorhexidine and polyhexamethylene biguanide against salivary staphylococcus aureus

OBJECTIVE: The aim of the present study was to determine the in vitro maximum inhibitory dilution (MID) of two chlorhexidinebased oral mouthwashes (CHX): Noplak®, Periogard®, and one polyhexamethylene biguanide-based mouthwash (PHMB): Sanifill Premium® against 28 field Staphylococcus aureus strains using the agar dilution method. MATERIALS AND METHODS: For each product, decimal dilutions ranging from 1/10 to 1/655,360 were prepared in distilled water and added to Mueller Hinton Agar culture medium. After homogenization, the culture medium was poured onto Petri dishes. Strains were inoculated using a Steers multipoint inoculator and dishes were incubated at 37ºC for 24hours. For reading, MID was considered as the maximum dilution of the mouthwash still capable of inhibiting microbial growth. RESULTS: Sanifill Premium® inhibited the growth of all strains at 1/40 dilution and of 1 strain at 1/80 dilution. Noplak® inhibited the growth of 23 strains at 1/640 dilution and of all 28 strains at 1/320 dilution. Periogard® showed inhibited growth of 7 strains at 1/640 dilution and of all 28 strains at 1/320 dilution. Data were submitted to Kruskal-Wallis statistical test, showing significant differences between the mouthwashes evaluated (p<0.05). No significant difference was found between Noplak® and Periogard® (p>0.05). Sanifill Premium® was the least effective (p<0.05). CONCLUSION: It was concluded that CHX-based mouthwashes present better antimicrobial activity against S. Aureus than the PHMB-based mouthwash.

Determination of the maximum inhibitory dilution of cetylpyridinium chloride-based mouthwashes against staphylococcus aureus: an in vitro study

The aim of this in vitro study was to determine the maximum inhibitory dilution (MID) of four cetylpyridinium chloride (CPC)-based mouthwashes: CPC+Propolis, CPC+Malva, CPC+Eucaliptol+Juá+Romã+Propolis (Natural Honey®) and CPC (Cepacol®), against 28 Staphylococcus aureus field strains, using the agar dilution method. Decimal dilutions ranging from 1/10 to 1/655,360 were prepared and added to Mueller Hinton Agar. Strains were inoculated using Steers multipoint inoculator. The inocula were seeded onto the surface of the culture medium in Petri dishes containing different dilutions of the mouthwashes. The dishes were incubated at 37ºC for 24 h. For readings, the MID was considered as the maximum dilution of mouthwash still capable of inhibiting microbial growth. The obtained data showed that CPC+Propolis had antimicrobial activity against 27 strains at 1/320 dilution and against all 28 strains at 1/160 dilution, CPC+Malva inhibited the growth of all 28 strains at 1/320 dilution, CPC+Eucaliptol+Juá+Romã+Propolis inhibited the growth of 2 strains at 1/640 dilution and all 28 strains at 1/320 dilution, and Cepacol® showed antimicrobial activity against 3 strains at 1/320 dilution and against all 28 strains at 1/160 dilution. Data were submitted to Kruskal-Wallis test, showing that the MID of Cepacol® was lower than that determined for the other products (p<0.05). In conclusion, CPC-mouthwashes showed antimicrobial activity against S. aureus and the addition of other substances to CPC improved its antimicrobial effect.

Analysis of contamination of endodontic absorbent paper points

PURPOSE: The aim of this study was to assess the contamination status of endodontic absorbent paper points from sterilized or not sterilized commercial packs, as well as paper points exposed to the dental office environment. METHODS: Twenty absorbent paper points were evaluated for contamination status packed under different conditions: commercial/sterilized pack, commercial/non-sterilized pack, exposed to the clinical environment, and intentionally contaminated (positive control). Contamination was determined qualitatively and quantitatively by aerobiosis, capnophilic growth, and pour plate. The Petri dishes were analyzed with a colony counter, and the results were expressed as colony-forming units. The data were analyzed by Kruskal-Wallis test (α=0.05). RESULTS: No difference in colony-forming units was found among the groups of endodontic absorbent paper points. All groups were contaminated by fungi and bacteria. CONCLUSION: It can be concluded that the sterilization of absorbent endodontic paper points before clinical use should be recommended regardless of commercial presentation

Filmes ultrafinos de ésteres de celulose: preparo, caracterização e imobilização de proteínas

In this study cellulose acetate butyrate (CAB) and carboxymehtylcellulose acetate butyrate (CMCAB) films adsorbed onto silicon wafers were characterized by means of ellipsometry, atomic force microscopy (AFM), sum frequency generation spectroscopy (SFG) and contact angle measurements. The adsorption behavior of lysozyme (LIS) or bovine serum albumin (BSA) onto CAB and CMCAB films was investigated. The amounts of adsorbed LIS or BSA onto CMCAB films were more pronounced than those onto CAB films due to the presence of carboxymethyl group in the CMCAB structure. Besides, the adsorption of BSA molecules on CMCAB films was more favored than that of LIS molecules. Antimicrobial effect of LIS bound to CAB or CMCAB layers was evaluated using Micrococcus luteus as substrate.