I am part of the Formal Methods Laboratory at CIn-UFPE.
My general research interests include software
evolution, refactoring, component-based software engineering, modeling,
MDA, development processes and formal methods.
Past Doings
Algebraic Transformation Laws for UML-RT
I acquired a M.Sc. degree from Federal University of Pernambuco(Informatics Center) in May, 2005, supervised by Augusto Sampaio and Alexandre Mota . The
main focus of the Master course was on Software Engineering, with the
master thesis Rigorous Development with UML-RT. The thesis proposed a
comprehensive set of laws that govern small changes in the main UML-RT (a
UML profile, with ADL characteristics, used to specify concurrent and
distributed systems) model views. From these basic laws, derived laws can
be taken as precise model refactorings that are
easily applied in a rigourous development, as
showed in this work, without the developer directly dealing with the
formalism that supports them. Also, this work assigned a
semantics for UML-RT via mapping into a formal notation. From this
semantics, we were able to show the correctness of those model
transformation laws and to show that they preserve system behaviour.
Click here for more
details about the M.Sc. Thesis.
Distributed Software Factories
One of my university projects resulted in a paper
showing lessons learned in the adaptation of a
traditional development process to software factories with distributed
teams. Some
agile principles are also considered.
Phoenix: A Test tool for EMS functionalities
I spent the first seven months of 2003 doing a full-time sequential course of Complementary Formation in Analysis of Software at Software Test Program - Motorola/Cin, Federal University of Pernambuco. This sequential course focused on the preparation of test engineers for mobile applications, with software engineering and mobile software architecture class courses and trainee activities. My course project was focused on the construction of a test tool for EMS functionalities of mobile phones. This tool was constructed based on information retrieved from a legacy system.
Automatic Generation of Java Assertions
To fulfill a partial requirement for the B.Sc. degree, I worked in one tool for automatic generate Java assertions (see Jass project) from formal specification in the Z notation, supervised by Augusto Sampaio. These assertions are used to dynamic identify constraint violations of the code, based on a previous Z specification.
|