[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Questionnaire about the tech scenario TLA+ is applied

Dear all:

   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! 

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/19e0a3cf-a6fa-4a09-9355-fc789a4f30e2%40googlegroups.com.