I am working in a telecom euipment manafacturing company and responsible for software architecture design and verification.
Our products mainly focuses on wireless access solutions, includes base station, cloud based Core Network and Infrastructure management systems.
In 2019, we introduced TLA+ into ne of our existing projects for trial.
This project is a middleware for distributed high performance datagram service. It is somewhat like kafka, but kafka can not fufill the real time and high Qos demands for
embedded CT applications, so we develpoed private communication protocol.
The first Spec aims to verfiy the the data consistency algorithm of the protocol, and we managed to find a hidden flaw which will occur in an unusal condition.
The second Spec aims to verify the ongoing design of the HA function, we also find one critical defect in switch over algorithm.
Now I want to introduce TLA+ to more other project teams. But I often face the argue from some team leaders such as " Can you prove TLA+ is suitable for the work of my tech stacks?".
Some of our staff also told me to verify public network protocols and open-source software compnents by TLA+, but I think this is the long term academic research and we should
concentrate on our self-developed software in short term.
I know TLA+ is capable of describe all discret event systems in theory, what I want to know is to get some info about your major field and why TLA+ is helpful for your major fields?
Your opinion will be highly appreciated, thanks a lot!