我正在从事一个医疗嵌入式系统项目，类似于输液泵。我们有一个初步的原型，我们正在进入项目的第二阶段。在这里，我们希望通过使用形式化方法做得更好。我有 CS 背景，但没有任何正式工具或语言的经验。我发现了一些来自宾夕法尼亚大学和亚利桑那州的出版物，他们在输液泵原型上使用了 Uppaal、AADL 等 ( http://www.fda.gov/medicaldevices/productsandmedicalprocedures/generalhospitaldevicesandsupplies/infusionpumps/ucm202511.htm )。我想向社区询问哪些工具或语言（最好是开源）可用于以下目的。
1) 目前，我们将 UI 屏幕作为状态机，并且有很多状态。是否有正式的工具来指定和嵌入算法以及这些屏幕？Z 或 TLA 可以用于此目的吗？
2) 我应该使用哪些工具和语言来描述软件架构和设计？我们没有 RTOS 或复杂的硬件，它只是微控制器。
3) 建模和验证控制算法和协议状态机的工具。
4) 从规范生成测试用例的工具。
我应该学习不同的语言或工具吗？是否有一套最小的工具可以满足上述要求？