Since this hasn't been mentioned yet, I'll mention it: you can maybe use
refinement. You start with an overly abstracted specification and some
properties that you check with TLC, then refine some aspects of the
specification. You can specify the implementation relation between the
two levels of abstraction.
Best regards,
Marko
Calvin Loncaric <c.a.loncaric@xxxxxxxxx> writes:
> You are both asking the hard questions. :)
>
> Regarding how to decompose the system: I don't know enough specifics to
> tell you whether to make one big specification or many small ones. Instead,
> I'll say a few very general things that work well for me when I'm making
> that choice in my own work:
>
> - Start with a correctness condition. Modeling any part of the system is
> wasted work unless you know what you'll be checking---and knowing what
> you'll be checking when you start will help identify what parts of the
> system are the most important.
> - Start small. Once you have written down what it means for the system
> to be right, you want to get as quickly as possible to a point where you
> can start model checking and building confidence. Elaborating a small
> starting specification is much easier than building a big one from scratch.
> (I also recommend taking notes during this process. Often things I write
> down like "TBD: does the source code actually check this condition?" or
> "Note: these two variables can't be read together atomically" turn out to
> be real bugs later. But don't get bogged down yet trying to read every line
> of source code or split up every non-atomic sequence of steps.)
> - Don't worry about state space explosion. Yes, it can be a real
> problem, but you will drive yourself insane if you try to worry about it
> from the outset. Get down a faithful specification first, and worry about
> the model checker second.
>
> Regarding integration testing: this could mean many things, and I'm not
> sure I'm on the same page about what you're hoping for. I *think* this is a
> question about how to make sure all the different plugins work together
> correctly, in which case my advice is the same as above: start with one
> spec, but start small and build up.
>
> --
> Calvin
>
>
> On Tue, Oct 11, 2022 at 10:40 AM hornace...@xxxxxxxxx <
> hornacek.martin@xxxxxxxxx> wrote:
>
>> Hi Morgan,
>>
>> Thank you for the hint with the BRMS framework, I will check which tools
>> are available and whether I could utilise them.
>> I am bit afraid how powerful those tools are, as the plug-in logic is
>> quite complex, but let's see.
>>
>> @Calvin: Good to hear that I am not completely barking up the wrong tree
>> here :)
>> I see Morgan's point though with the concern how to approach the system
>> specification, i.e. one large spec vs or one spec per plug-in, but thinking
>> about it I would say the solution would be somewhere in the middle.
>> I can imagine grouping the plug-in business logic to non-overlapping
>> "modules" and having one spec per "module".
>>
>> The "integration testing" aspect is indeed what I (maybe due to lack of
>> experience) cannot still envision.
>> Maybe I need to just study the existing specs and see if I will be able to
>> come up with a sample spec that would model "my" system and go from there...
>>
>> M.
>>
>> Dátum: utorok 11. októbra 2022, čas: 6:33:40 UTC+2, odosielateľ:
>> morgan....@xxxxxxxxx
>>
>>> Hi Calvin,
>>>
>>> I'm also a TLA+ beginner, just anticipating the next question... how
>>> would integration testing work? Martin mentioned that he had a lot of
>>> plug-ins, so would he have a 1:1 mapping of plug-in to spec, or one large
>>> spec including logic from all plug-ins?
>>>
>>> It seems like there would be a state-space explosion with the second
>>> option, but then I can't see how the first option would test that one
>>> plug-in didn't affect the others.
>>>
>>> many thanks
>>>
>>>
>>> On Tue, Oct 11, 2022 at 9:49 AM Calvin Loncaric <c.a.lo...@xxxxxxxxx>
>>> wrote:
>>>
>>>> I absolutely think TLA+ is applicable to your situation.
>>>>
>>>> TLA+ is often presented as a tool for designing distributed
>>>> systems---but what makes it great for designing distributed systems also
>>>> makes it great for designing plugins:
>>>>
>>>> - The system is composed of an environment and a program (e.g. the
>>>> network and a cluster of servers, or in your case Dynamics 365 and your
>>>> plugin)
>>>> - The environment drives events (e.g. packet delivery, or in your
>>>> case the events that the plugin responds to)
>>>> - Testing the program is impractical because there is no easy way to
>>>> exercise all the possible behaviors of the environment
>>>>
>>>> ...although, this shouldn't be news to you; it sounds like you've
>>>> already guessed how TLA+ can help: "[...] the system could be viewed as
>>>> black box where the events transform the system from one state to another.
>>>> Ideally we would like to check that the state of the system after an event
>>>> is 'correct' as a result of the plug-in logic".
>>>>
>>>> In the best possible case, a TLA+ spec can serve as a precise design
>>>> document that details what you believe to be true about the environment and
>>>> lets you quickly evaluate possible changes to the plugin logic.
>>>>
>>>> --
>>>> Calvin
>>>>
>>>>
>>>>
>>>> On Sun, Oct 9, 2022 at 11:01 AM hornace...@xxxxxxxxx <
>>>> hornace...@xxxxxxxxx> wrote:
>>>>
>>>>> Hello everyone,
>>>>>
>>>>> I am looking for some advice regarding TLA+, in particular in
>>>>> evaluating if could be the right tool for my problem. My experience with
>>>>> TLA+ is quite limited so I figured I'd ask people with more experience for
>>>>> advice.
>>>>>
>>>>> On my current assignment, I am working with Dynamics 365 CE system.
>>>>> This system allows to develop a plug-in with custom business logic to
>>>>> modify or augment the standard behavior of the platform. Plug-ins are
>>>>> essentially handlers for events fired by Dynamics 365 Customer Engagement .
>>>>> You can subscribe, or register, a plug-in to a known set of events to have
>>>>> your code run when the event occurs.
>>>>>
>>>>> For example, when user is creating an Opportunity entity record in the
>>>>> system, the system determines the Default Price List for the current user
>>>>> and sets this value on the newly created record.
>>>>>
>>>>> Our implementation relies heavily on these customizations, i.e. there
>>>>> lot of plug-ins in the system with business logic that supports pricing and
>>>>> financing use cases, approval workflows, etc.
>>>>>
>>>>> My main concern is mainly these points:
>>>>>
>>>>> - Currently, we have no overview about the chain of events
>>>>> happening in the system. Imagine situations like a certain plug-in logic
>>>>> being fired twice resulting in wrong calculations as an end result,
>>>>> infinite loops, unnecessary wait times for some of the events etc.
>>>>> - Testability of the system in general. The plug-in code is tested
>>>>> by unit test, but these won't test the behavior of the plug-in within the
>>>>> platform. We developed a set of Integration tests, that exercises the
>>>>> plug-in logic by invoking the events that should trigger the plug-in logic.
>>>>> From the example I've given above, the test will arrange a particular
>>>>> system state, send a Create request for Opportunity entity record and
>>>>> assert if the Price List value matches the expected Default Price List
>>>>> value hence verifying the system behavior.
>>>>> - The plug-in code turned into a big ball of mud. The developers
>>>>> are afraid to touch some of the plug-in code with fear to introduce bugs
>>>>> when developing new features for critical business logic related to pricing
>>>>> or financing. The Integration tests I mentioned above provide a safety net,
>>>>> but they don't guarantee that in certain edge cases a bug hasn't slipped
>>>>> into the system.
>>>>>
>>>>> What I strive for is to really gain confidence about the system
>>>>> behavior and avoid subtle bugs. From my perspective, the system could be
>>>>> viewed as black box where the events transform the system from one state to
>>>>> another. Ideally we would like to check that the state of the system after
>>>>> an event is "correct" as a result of the plug-in logic.
>>>>>
>>>>> Does someone see a possibility that TLA+ could be a useful tool in this
>>>>> context? Maybe some tools which would support property-based testing would
>>>>> be more appropriate in this case, but I am still searching...
>>>>>
>>>>> So far, I only experimented a bit with TLA+ as interesting pastime
>>>>> project. I found it both interesting and powerful, but it never occurred to
>>>>> me to use it as part of my current role as I simply thought that it is
>>>>> suited to solve problems in a completely different domain.
>>>>> I wish a knew about it while is writing my diploma thesis on network
>>>>> coding for distributed storage systems though. It would save me some time.
>>>>>
>>>>> Thank you for you opinions.
>>>>> Martin
>>>>>
>>>>> --
>>>>> 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...@xxxxxxxxxxxxxxxx.
>>>>> To view this discussion on the web visit
>>>>> https://groups.google.com/d/msgid/tlaplus/809a0575-f6da-4875-b35f-67bef473aafdn%40googlegroups.com
>>>>> <https://groups.google.com/d/msgid/tlaplus/809a0575-f6da-4875-b35f-67bef473aafdn%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>> .
>>>>>
>>>> --
>>>> 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...@xxxxxxxxxxxxxxxx.
>>>>
>>> To view this discussion on the web visit
>>>> https://groups.google.com/d/msgid/tlaplus/CABf5HMjXL9ohn71ydu5eWzucRWe%2BUBvuscDonQGeFvUDWeCJ1Q%40mail.gmail.com
>>>> <https://groups.google.com/d/msgid/tlaplus/CABf5HMjXL9ohn71ydu5eWzucRWe%2BUBvuscDonQGeFvUDWeCJ1Q%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>>> .
>>>>
>>> --
>> 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 view this discussion on the web visit
>> https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com
>> <https://groups.google.com/d/msgid/tlaplus/8912c99e-4bf1-4bd9-a51c-bd66af265783n%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
> --
> 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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABf5HMgd5yDYtja9GfbcaXRCA1cbCA6bTX45x-Rx%3DaCHK1Mj3A%40mail.gmail.com.
--
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681
--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87mt9ytjji.fsf%40manjaro.mail-host-address-is-not-set.