|
|
SCXML state machine interpretter
Baláž, Ján ; Parízek, Pavel (referee) ; Šerý, Ondřej (advisor)
Currently there is a need for programmers to access various tasks with alternative procedures. One such practice is using the state machine entry. As the solution shows a newly emerging standard by W3 Consorcium, called SCXML. By now, there are several di fferent implementation, but because of their robustness may not be suitable for individuals or small to medium businesses. These companies need tools that can easily adapt to their own projects. The aim of this work is to create a state machine interpreter described SCXML language that will satisfy the conditions described. The e ort is to implement the maximal part of SCXML specification. Work will be created in Perl and will support the operating systems Windows and Linux.
|
|
|
Model Checking and Reduction of Behavior Protocols
Šerý, Ondřej ; Bednárek, David (referee) ; Plášil, František (advisor)
Behavior protocol is a formalism used for behavior specification of software components. In a regular-expression like syntax, admissible sequences of method invocations are specified abstracting from components' internal data. While it seems to be a reasonable level of abstraction for checking correctness of communication of the software components, it can be still quite difficult for a human to read and understand. This thesis aims to help the software designer to understand the behavior specification of components more easily. An approach to automatic verification of the general temporal properties stated in Linear Temporal Logic is presented along with two techniques for reduction of behavior protocols. Reduction with respect to composition prunes out those parts of the protocols that are not used in the particular composition and vlarifies the actual role of each component. Reduction with respect to property removes the parts of the protocols that are irrelevant to the given property. The behavior protocols reduced in this manner should emphasize which part of the protocol makes the given property satisfied.
|
|
|
Influence of inhaled manganese oxides nanoparticles on mass of internal organs in mice
Zeman, T. ; Dočekal, Bohumil ; Mikuška, Pavel ; Buchtová, Marcela ; Míšek, Ivan ; Šerý, Omar ; Večeřa, Zbyněk
Results of the statistical analysis of a long-term inhalation experiment on laboratory mice are presented. During 17 weeks of the experiment, the experimental group was exposed to inhaled manganese oxides nanoparticles. Manganese oxides (MnO center dot Mn2O3) nanoparticles (MnONPs) were synthesized continuously via aerosol route in a hot wall tube flow reactor using a thermal decomposition of metal organic precursor manganese(II) acetylacetonate in the flow tube reactor (in vertical position) at temperature 750 degrees C in the presence of 30 vol% of oxygen. The concentration of produced MnONPs at the reactor output was in the range 1-3 x 10(7) particles/cm(3) and the size of generated nanoparticles MnO center dot Mn2O3 was in the range 7-50 nm. Before entering the inhalation chamber, MnONPs in the mixture of N-2, O-2 and air (at total flow rate of 3 L/min) were further diluted using filtrated humidified air (20 L/min) at temperature 21 degrees C resulting in the MnONPs concentration 2 x 10(6) particles/cm(3). At regular time intervals the mass of selected internal organs of mice from both experimental and control group was assessed. It has been proven that inhaled nanoparticles are able to influence the mass of internal organs of mice. Statistically significantly lower mass of kidneys, liver and spleen and higher mass of pancreas have been found in the experimental group compared to the control group.
|
|
|
Influence of inhaled manganese oxides nanoparticles on mass of internal organs in mice
Zeman, T. ; Dočekal, Bohumil ; Mikuška, Pavel ; Buchtová, Marcela ; Míšek, Ivan ; Šerý, Omar ; Večeřa, Zbyněk
Results of the statistical analysis of a long-term inhalation experiment on laboratory mice are presented. During 17 weeks of the experiment, the experimental group was exposed to inhaled manganese oxides nanoparticles. Manganese oxides (MnO.Mn2O3) nanoparticles (MnONPs) were synthesized continuously via aerosol route in a hot wall tube flow reactor using a thermal decomposition of metal organic precursor manganese(II)acetylacetonate in the flow tube reactor (in vertical position) at temperature 750 °C in the presence of 30 vol% of oxygen. The concentration of produced MnONPs at the reactor output was in the range 1-3 × 107 particles/cm3 and the size of generated nanoparticles MnO.Mn2O3 was in the range 7-50 nm. Before entering the inhalation chamber, MnONPs in the mixture of N2, O2 and air (at total flow rate of 3 L/min) were further diluted using filtrated humidified air (20 L/min) at temperature 21 °C resulting in the MnONPs concentration 2 × 106 particles/cm3. At regular time intervals the mass of selected internal organs of mice from both experimental and control group was assessed. It has been proven that inhaled nanoparticles are able to influence the mass of internal organs of mice. Statistically significantly lower mass of kidneys, liver and spleen and higher mass of pancreas have been found in the experimental group compared to the control group.
|
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
Slicing specifikace chování komponent
Šerý, O. ; Plášil, František
Being an important means of reducing development costs, behavior specification of software components facilitates reuse of a component and even reuse of a component’s architecture (assembly). However, since typically only a part of the components’ functionality is actually used in the new context, a significant part of the behavior specification may be superfluous. As a result, it may be hard to see (and filter out) the actual interplay among the components in their behavior specification. This paper targets the problem in the scope of behavior protocols [13]. It presents a technique for slicing behavior protocols with respect to a given context (composition), designed to remove the unused behavior from a behavior specification. The technique is based on a formal foundation, generic enough to support slicing with respect to a property expressed as a predicate. To demonstrate viability of the proposed approach, a positive experience with behavior specification slicing applied in real-li
|
guest ::
RSS feed.