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.lo...@gmail.com> 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
>>>> - 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
>>>>> - 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
>>>>> <
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...@googlegroups.com.
>>>>
>>> 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+u...@googlegroups.com.
>> 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+u...@googlegroups.com.
> 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