Applicability of TLA+ to the design of electronic circuits and systems?

[whitewaters...@gmail.com]

Hello everyone,

Hypothetically, lets assume that I am designing a circuitry to control a fuel solenoid in a commercial airliner. The circuit takes a number of analog and digital inputs (1 or 0), processes them, and then controls an electric motor which actuates the valve to open or close.

At a high level the system is organized as different functional blocks with inputs , outputs, and a certain defined behavior. Unlike a typical computer program each of the blocks is "asynchronous." Different blocks are connected together to get a certain behavior from the system.

My goal is to show that the functional blocks work together to produce a deterministic well defined behavior. (eg. it opens when commanded to open, closes when commanded to close, etc.)

For reference some inputs/outputs are digital (false=0, or true=1) and others are analog (eg. 0.0 to 1.2345).


I have two questions:
* Can TLA+ represent "analog" and "digital" signals? (eg. an amplifier with a gain of 2 would take and input of 1.1 and output 2.2, or a digital AND gate would take two 0 or 1 digital inputs and produce a single 0 or 1 digital output)
* Is TLA+ a suitable tool to analyze an "asynchronous" analog/digital system similar to what I have described?

Thanks Everyone,
-Jason White

[Amir A.H.S.A]

Hi,

TLA+ has a module named "Real" which precisely defines the set of all real numbers, so you can include that module in your specification and you can use a variable x \in Real to represent the voltage values.

As to your specific question about whether or not you can specify asynchronous parts of your system in TLA+, the answer is a absolute Yes.

TLA+ is specifically designed for formal specification and verification of concurrent systems, both synchronous and asynchronous ones.

My suggestion is that you study the first three chapters of the TLA+ book as a start, which you can download from this hyperlink: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf

Regards,

AmirHossein

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0577e562-c902-474d-8757-846ee737be0b%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

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