Path: csiph.com!eternal-september.org!feeder.eternal-september.org!reader02.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.arch.embedded
Subject: Re: When exactly do you choose to use a RTOS (instead of a non-OS approach)?
Date: Sun, 07 Jan 2018 00:39:51 -0800
Organization: A noiseless patient Spider
Lines: 22
Message-ID: <87efn23vvs.fsf@nightsong.com>
References: <p0h1kt$tb7$1@dont-email.me> <p0jhvg$bb7$1@news2.open-news-network.org> <p13mob$dfn$2@dont-email.me> <ad8c675d-61e1-4e64-b511-af822e8ec1b8@googlegroups.com> <p1bg2u$5ke$2@dont-email.me> <p2igr5$j9j$1@dont-email.me> <p2j5mn$bev$2@dont-email.me> <p2jqj6$9jq$1@dont-email.me> <p2kotf$cu9$1@dont-email.me> <p2lve0$tuv$1@dont-email.me> <%jH3C.197195$nS6.171613@fx23.am4> <p2pfkf$7or$1@dont-email.me> <Hu04C.396964$Gr2.167584@fx36.am4> <p2risv$fe5$2@dont-email.me> <_se4C.151323$OX.8147@fx47.am4> <87o9m6wj2z.fsf@nightsong.com> <i3f4C.238605$p_5.199049@fx05.am4>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org; posting-host="ae97e3878acaa56b84b352c4f0fedc83"; logging-data="30070"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18J5xD3XgMae4Rqyg1+CpsF"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/25.3 (gnu/linux)
Cancel-Lock: sha1:zjAW2Rj0s/RrGX10INZPzsBFBOQ= sha1:ZJtB6ibIaUVb7VZnB4CCYfmoxLE=
Xref: csiph.com comp.arch.embedded:27537

Tom Gardner <spamjunk@blueyonder.co.uk> writes:
> Hence I'd like to see some independent assessment on some _existing_
> real-world protocols/FSMs.

I don't know where to find any of those.  Got any suggestions?

> Failing that, how do their techniques perform when developing _new_
> protocols/FSMs? If they are generally a help, then that would be
> great!

I'd be interested to know what you think of ImProve.  The link I gave
earlier:

  https://github.com/tomahawkins/improve/wiki/ImProve

I'd look at the "verification primer" section to get an idea of what it
does.  Don't worry about understanding the syntax etc, which takes some
getting used to.

The basic approach is to control the state space explosion using a SAT
solver.  Those have gotten very powerful in recent years.  They might
get even more powerful with reinforcement learning techniques soon.