[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.