TLA+ can specify essentially any system that you can describe
precisely. Writing a precise desription of a system helps you to
understand it, having a precise language like TLA+ with a parser that
can keep you from writing complete nonsense can be a help. However,
most engineers are interested in using tools to help them find
nontrivial errors. And your description of what you want to do is too
vague to indicate whether the TLA+ tools can help you.
First of all, be aware that although there is a standard Reals module,
TLC can't handle a spec that uses it. Moreover, the TLAPS back-end
provers have no built-in knowledge of real numbers. One can add the
necessary axioms, but writing proofs of nontrivial properties might be
quite tedious. Fortunately, there should be no need to do that.
Assuming discrete time should suffice. (Wouuld your system really
stop working if time were quantized and no two separate events that
didn't happen at exactly the same time could occur less than one
femtosecond apart?)
A simple, old, practical approach to specifying real-time systems is
described in my paper "Real Time is Really Simple". That paper also
describes a way to model check such systems, but to my knowledge it
hasn't been used on any real example. Adding real-valued physical
quantities shouldn't change things. You might want to look at my
paper "Hybrid Systems in TLA+".
Leslie