Especificação Formal - Problema Pedágio - Lógica para computação

Especifica¸ao Formal do Sistema de Fiscaliza¸ao c˜ c˜ de Ped´gio a Bruno Milhan de Oliveira (Sistemas de Informa¸˜o) ca 29 de setembro de 2013
Resumo
A cobran¸a de ped´gio em estradas brasileiras ´ um tema cercado de c a e polˆmica, suspeitas e questionamentos. Diante disso, ´ preciso rigor no que e e diz respeito a transparˆncia, fiscaliza¸ao e regulamenta¸˜o. No Paran´,
`
e c˜ ca a as tarifas que podem ser cobradas s˜o definidas no contrato de concess˜o, a a podendo ser reajustadas anualmente. A fiscaliza¸ao do servi¸o cabe ao c˜ c
DER PR – Departamento de Estradas de Rodagem do Estado do Paran´. a Suponha que ex-funcion´rios de uma concession´ria tenham denunciado a a um esquema de fraude as autoridades. A concession´ria estaria repassando
`
a dados incorretos ao org˜o fiscalizador, com n´meros de ve´
´ a u ıculos menores do que os reais. Isso seria feito manipulando a abertura e o fechamento das cancelas. Desta forma, os lucros seriam maiores que osdeclarados.
Diante das den´ncias, o seu grupo foi contratado para desenvolver um u sistema adicional para contagem dos ve´ ıculos em uma pra¸a de ped´gio. c a
A ideia ´ espalhar cˆmeras em pontos altos, obtendo uma vis˜o a´rea do e a a e ambiente. O sistema deve interpretar as imagens, contando e classificando os ve´ ıculos que passam a cada instante. Os dados gerados pelo sistema podem ent˜o ser comparados aqueles fornecidos pela concession´ria. A a ` a inten¸ao das autoridades ´ usar o mesmo sistema em todas as pra¸as de c˜ e c ped´gio do estado. a 1

Sum´rio a 1 Descri¸˜o Textual ca 3

2 Especifica¸˜o Formal ca 2.1 Tipos do sistema . . . . . . . . . . . . . . . . . . . . . . .
2.2 Estado do sistema . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Nome do sistema e descri¸˜o dos itens do estado do ca 2.2.2 Inicializa¸˜o do estado do sistema . . . . . . . . . ca 2.3 Fun¸˜es e predicados definidos . . . . . . . . . . . . . . . co 2.3.1