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

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

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.