Re: [tlaplus] Applicability of TLA+ to the design of electronic circuits and systems?

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

On Fri, May 31, 2019 at 12:08 AM <whitewaterssoftwareinfo@xxxxxxxxx> wrote:

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

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
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.