scholarly journals From UML to Petri Nets for non functional Property Verification

2006 ◽  
Author(s):  
F. Mallet ◽  
M-A. Peraldi-Frati ◽  
C. Andre
Keyword(s):  
Petri Nets ◽  
Functional Property ◽  
Property Verification

Merging and Splitting Petri Net Models within Distributed Embedded Controller Design

2013 ◽  
pp. 160-183 ◽  
Author(s):  
Luis Gomes ◽  
Anikó Costa ◽  
João Paulo Barros ◽  
Filipe Moutinho ◽  
Fernando Pereira
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Code Generation ◽  
Controller Design ◽  
Output Place ◽  
Time Domains ◽  
Splitting Operation ◽  
Embedded Controller ◽  
Automatic Code ◽  
Property Verification

Design of distributed embedded controllers can benefit from the adoption of a model-based development attitude, where Petri nets modeling can provide support for a comprehensive specification and documentation of the system together with verification capabilities and automatic deployment into implementation platforms. This chapter presents a Petri nets-based development flow based on composition and decomposition of Petri net models, using Input-Output Place-Transition Petri nets (IOPT nets) as the underlying formalism, allowing reusability of models in new situations through a net addition operation, as well as partitioning of the model into components using a net splitting operation. Distributed embedded controllers are addressed adding the concept of time domains to IOPT nets. Finally, a tool chain framework is presented supporting the whole development process, from specification to implementation, including property verification, simulation, and automatic code generation for deployment into implementation platforms (considering hardware-based implementation and VHDL coding or software-oriented implementation and C coding).

scholarly journals Patterns of Regional Brain Hypometabolism Associated with Knowledge of Semantic Features and Categories in Alzheimer's Disease

2006 ◽  
Vol 18 (12) ◽  
pp. 2138-2151 ◽  
Author(s):  
Roland Zahn ◽  
Peter Garrard ◽  
Jochen Talazko ◽  
Matthias Gondan ◽  
Philine Bubrowski ◽  
...  
Keyword(s):  
Alzheimer’S Disease ◽  
Alzheimer's Disease ◽  
Semantic Memory ◽  
Functional Properties ◽  
Functional Property ◽  
Semantic Knowledge ◽  
Brain Areas ◽  
Functional Features ◽  
Property Verification ◽  
Living Objects

The study of semantic memory in patients with Alzheimer's disease (AD) has raised important questions about the representation of conceptual knowledge in the human brain. It is still unknown whether semantic memory impairments are caused by localized damage to specialized regions or by diffuse damage to distributed representations within nonspecialized brain areas. To our knowledge, there have been no direct correlations of neuroimaging of in vivo brain function in AD with performance on tasks differentially addressing visual and functional knowledge of living and nonliving concepts. We used a semantic verification task and resting 18-fluorodeoxyglucose positron emission tomography in a group of mild to moderate AD patients to investigate this issue. The four task conditions required semantic knowledge of (1) visual, (2) functional properties of living objects, and (3) visual or (4) functional properties of nonliving objects. Visual property verification of living objects was significantly correlated with left posterior fusiform gyrus metabolism (Brodmann's area [BA] 37/19). Effects of visual and functional property verification for non-living objects largely overlapped in the left anterior temporal (BA 38/20) and bilateral premotor areas (BA 6), with the visual condition extending more into left lateral precentral areas. There were no associations with functional property verification for living concepts. Our results provide strong support for anatomically separable representations of living and nonliving concepts, as well as visual feature knowledge of living objects, and against distributed accounts of semantic memory that view visual and functional features of living and nonliving objects as distributed across a common set of brain areas.

scholarly journals Improving Synchronous Dataflow Analysis Supported by Petri Net Mappings

Electronics ◽  
2018 ◽  
Vol 7 (12) ◽  
pp. 448
Author(s):  
José-Inácio Rocha ◽  
Octávio Páscoa Dias ◽  
Luís Gomes
Keyword(s):  
Petri Nets ◽  
Petri Net ◽  
Initial Conditions ◽  
Digital Signal ◽  
Industrial Applications ◽  
New Approach ◽  
Synchronous Dataflow ◽  
Model Driven ◽  
Property Verification ◽  
Static Schedule

Whereas most of the work that analyses Synchronous Dataflow (SDF) stays in the dataflow framework, this work pushes its analysis into another framework level, thereby addressing issues that are not well addressed or are even unexplored in SDF. In this manner, the paper proposes a model-driven engineering (MDE) method, combining Synchronous Dataflow (SDF) and Petri nets, to highlight and reinforce their interoperability in digital signal processing applications, cyber-physical systems, or industrial applications. Improvements regarding the settlement and exploitation of the initial conditions associated with SDF are demonstrated; this issue is crucial for every cyber-physical system, since a system’s initial conditions are crucial to ensuring the system’s liveness. The improvements outlined in this work exploit an innovating mapping in the Place/Transition (P/T) Petri net domain that is intended to reduce and predict the total amount of initial data in SDF channels. The relevance of the firing semantics engaged with the equivalent Petri net model is discussed. This paper proposes a new approach to estimate whether an SDF has a static schedule by performing simulation and property verification of the equivalent-based P/T Petri net system achieved, framed by a Petri net invariant analysis and based on the stubborn set method of Petri nets. In this way, this new approach will allow mitigating the state explosion problem. Finally, a strategy is applied to two case studies to discover all the elementary circuits (static schedules) associated with the generated model’s state-space.

Sign in / Sign up

Export Citation Format

Share Document