DesignLab
  • Departamento de Engenharia Mecatrônica
    Escola Politécnica - Universidade de São Paulo

Formal verification & Petri Nets

Grupo de Pesquisa

     The Formal Verification & Petri Nets Group is concerned with the use of formal approaches to Engineering Design -, especially to automated systems. The goal is to develop methods for analysis and design associated with Model-Based Engineering using Petri Nets (PN). We use PN-approaches based on the standard ISO/IEC 15.909, which defines classic Place/Transition nets and High-Level Nets, a transfer language - PNML - and several user extensions. The main goal is focused on extensions and its formalization following the standard. 

Extensions are hierarchy,  time slice, and Time Petri Nets. Verification approaches can be based on model-checking, property analysis, and/or invariants.   

Applications would include embedded information systems and (discrete) control, workflow, and to particular domains such as Smart Homes or  Smart Grids.

Atualizado em 03 de Julho de 2024, 22:49

Pesquisador Responsável


Jose Reinaldo Silva

reinaldo@usp.br

Bachelor in Physics from Bahia Federal University, got aMSc in Physics from Pernanbuco Federal University UFPE, and a MA in Computer Science from Mills College, USA. PhD in Computer Engineering by Universith of São Paulo and postdoc in Computer Science and in Systems Design Engineering at University of Waterloo, Ca. Research interests are in Engineering Systems Design, Requirements Engineering, Service Design Management and Engineering, Artificial Intelligence, Planning & Scheduling, Formal Verification methods, Data Spaces and Digital Transformation towards Industry 4.0.

Colaboradores


Javier Martinez Silva

javier.cu@gmail.com

Graduated in Computer Science from Universidad de Oriente, Cuba and received a Master in Computer Science from this same institution. Ph.D. in Mechatronics (Mechanical Control and Automation) from Escola Politécnica, USP, working with D-Lab. Postdoc in D-Lab, where he also acted on implementing the USP-AWS agreement. His research interests are in formal methods for modeling and analysis of requirements in automation projects and working with AI Planning to design modeling. Worked in the Samsung Research Center and is now working in Instituto Eldorado, another research institution linking the academy and the market.

José Jean-Paul Z. S. Tavares

jean.tavares@ufu.br

Graduated as a Mechanical Engineer at Escola Politécnica da USP and concluded a Master in Science and a Ph.D. at the same institutions. His research interests are in industrial process automation and IIoT, focusing on the identification of industrial targets using RFID. Studied the process of blank manufacturing to identify faults even before the IIoT term became popular. In his postdoc (also in D-Lab) started to improve more information in target identification enhancing local memory and including process information in Petri Net, composing a new tagged net, and adding AI Planning to the process. Today he is an Adjunct professor at the Universidade Federal de Uberlândia, leading the Manufacturing Automation Planning Lab.

Matheus Alexandrino Brito

matheus.a.brito12@usp.br

Matheus is a undergad student in the Mechatronics course and has a scholarship from USP, associated to D-Lab. His interests are in automation processes, particularly those involving Artificial Intelligence and AI Planning. Therefore, he join the research line in AI Planning and Machine Intelligence and do the project DiPlant (Didatic Planning Tool) - a system for analyzing plans (or post-planning) expected to be used in the undergrad course PMR3510 Inteligência Artificial.

Miguel Orellana Postigo

brc02847@usp.br

Mechanical & Electrician Engineer at the National University of San Agustín - Peru, Specialist in Maintenance Management at the Federal University of Amazonas, MBA in Project Management at Gama Filho University, MSc in Electrical Engineering at Escola Politécnica at USP. Currently, pursuing a Ph.D. in Mechatronics Engineering from the Polytechnic School of USP. Got a position of Professor Assistant - B since 2013, in the Department of Electrical Engineering / Electronics (EST) at University Amazonas state UEA. Research interests are in Industrial Automation, Smart Grid systems, Systems design, formal modeling methods.

Yaney Gomez Correa

ygc8104@usp.br

Graduate in Automatic Control at Universidade de Oriente, Cuba, and worked in automated systems associated to power supply and petroleum in this country. Got a MSc. at D-Lab in the subject of Service Automation Design applied to Healthcare, proposing assistant services on top of a building and residence automation. Ph.D. student at D-Lab working in Model-based Requirements and Hierarchical AI Planning.

Projetos


Arquivos