Dear All;
I am specifying a program to control an physical experiment using TLA+. I think I have my first draft, but of course there is a large room to improvements. I've tried to split the chunks of the specification it is not reliable, but the result appeared very cryptic. So I'm posting the documentation link that contains the specification:
http://dcm.ffclrp.usp.br/~aholanda/pidcon/pidcon.pdf
Some doubts:
1. At page 8 the function "DoPerodicMeasures" is specified, but now that I am studying temporal formulas, it seems to me that I can use them to specify this function. But a doubt occurred to me, when I specify using temporal formulas, some instructions necessary to the implementation are "coupled" into the formulas, it maybe is good in the specification, but the implementation loose a guide.
2. I think I put a lot of implementation details, mainly in the "CondutivityExperiment" specification.
3. I have doubts if "DeviceInterface" is being a good abstraction for the devices.
I have to apologize the draft state of the material, but I need some feedback to advance.
Any help are welcome.
Thanks in advance;
Regards;
Adriano.