Encontrados 7 documentos, a visualizar página 1 de 1
The APEX framework : prototyping of ubiquitous environments based on Petri Nets
Silva, José Luís Cardoso; Ribeiro, Óscar R.; Campos, J. Creissac; Fernandes, João M.; Harrison, M. D.The user experience of ubiquitous environments is a determining factor in their success. The characteristics of such systems must be explored as early as possible to anticipate potential user problems, and to reduce the cost of redesign. However, the development of early prototypes to be evaluated in the target environment can be disruptive to the ongoing system and therefore unacceptable. This paper reports on...
Animation-based validation of reactive software systems using behavioural models
Ribeiro, Óscar R.Tese de doutoramento em Informática ; During the development of software systems, validation is a crucial activity to guarantee that the software system ful lls the users' needs and expectations. A key issue to have a successful validation consists in adopting a process where users and clients can actively discuss the requirements of the system under development. A reactive system is expected to continuously i...
Validation of scenario-based business requirements with Coloured Petri Nets
Ribeiro, Óscar R.; Fernandes, João M.A scenario can be used to describe a possible instantiation of a given business use case and can be expressed for example as a list of steps written in natural language, or by an interaction diagram. This paper discusses how a collection of scenarios, all expressed as UML2 sequence diagrams, can be described for validation purposes by a single model, written in the Coloured Petri Nets (CPN) modelling language. ...
Designing tool support for translating use cases and UML 2.0 Sequence Diagrams ...
Fernandes, João M.; Tjell, Simon; Jorgensen, Jens B.; Ribeiro, Óscar R.Using a case study on the specification of an elevator controller, this paper presents an approach that can translate given UML descriptions into a Coloured Petri Net (CPN) model. The UML descriptions must be specified in the form of Use Cases and UML 2.0 Sequence Diagrams. The CPN model constitutes one single, coherent and executable representation of all possible behaviours that are specified by the given UML...
Validation of reactive software from scenario-based models
Ribeiro, Óscar R.; Fernandes, João M.This thesis proposal suggests a model-based approach to obtain, from a set of behavioural scenarios of a given reactive software system, a graphical animation for reproducing that set of scenarios for validation purposes. The approach assumes that the requirements of the system are described by a use case diagram, being the behaviour of each use case detailed by a collection of scenario descriptions. These use ...
Translating synchronous Petri Nets into PROMELA for verifying behavioural prope...
Ribeiro, Óscar R.; Fernandes, João M.For developing embedded systems, the design process may benefit in some contexts from the usage of formal methods, namely to find critical errors and flaws, before final design and implementation decisions are taken. The Synchronous and Interpreted Petri Net (SIP-net) modelling language is considered in this article to model embedded systems. This model of computation is based on safe Petri nets with guarded tr...
Model checking embedded systems with PROMELA
Ribeiro, Óscar R.; Fernandes, João M.; Pinto, Luís F.Comunicação apresentada ao IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), 12, Washington, 2005. ; The design process for embedded systems can benefit from the usage of formal methods, if some properties of the systems are checked, before design and implementation decisions are accomplished. This paper presents a model checking approach using the Spin tool, ...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||