Librería Samer Atenea
Kálamo Books
Librería Elías (Asturias)
Librería Kolima (Madrid)
Librería Proteo (Málaga)
Este livro centra-se na utilização do Event-B como método formal para a modelagem e verificação de software. O nosso estudo de caso é o sistema de controlo de elevadores (ECS). Os requisitos do elevador são traduzidos em modelos matemáticos Event-B. Utilizamos o RODIN para desenvolver, testar e verificar os modelos Event-B do ECS antes de podermos implementar o sistema num programa de software. A modelação em Event-B é tão vital que nos permite identificar requisitos em falta, erros no nosso projeto e comprovar que o modelo do sistema funcionará conforme o esperado, ao contrário do que aconteceria se desenvolvêssemos um sistema imediatamente após recebermos os requisitos do cliente. Estes requisitos são incompletos e ambíguos. Com a utilização do Event-B, reduzimos o custo do desenvolvimento do sistema, uma vez que os erros serão sempre detetados nas fases iniciais do desenvolvimento. A transição da fase de requisitos para a fase de especificação formal é um dos passos mais desafiantes. Na verdade, a construção de modelos iniciais a partir dos requisitos do sistema requer um elevado nível de competência e competências práticas em modelação Event-B. Uma vez que não existe um processo bem definido para orientar os engenheiros de sistemas, este livro fornece uma abordagem prática sobre como desenvolver bons sistemas de software.
