4 ms·

Can anyone recommend any links/articles/books about the relationships between specification, implementation, testing, provability, TDD, BDD, etc.? I have been

Can anyone recommend any links/articles/books about the relationships between specification, implementation, testing, provability, TDD, BDD, etc.? I have been working on designing some software for improving the specifications process, and quickly realized that it's a very interconnected concept: the specification can be treated very formally, leading to things like BDD (behavior-driven development), but also to things like formal provability. I'm generally interested in the relationships/processes that mediate between design <-> specification <-> actual programming. In reality, there's a lot of feedback, and I want to create ways of radically improving these processes.

throwawayjava 9y ago
You might be interested in this study as a way of refining your interests and goals: http://loonwerks.com/publications/pdf/cofer2013fmics.pdf http://loonwerks.com/publications/pdf/cofer2013fmics.pdf It's a big world out there; this has been an active area of research basically since Turing. Many of the "relationship between" questions you ask have their own conference or workshop series. > formal provability IMO the best way to start down this road is to just begin using some of the tools out there -- TLA+, Coq, whatever - and touch base with the community around your choice of tool (conferences, workshops, or even going back to school for a phd). The best way to learn about the strengths and limitations of current software practice is to sit down and churn out code, preferably with a strong mentor. The same is true for proof programming.
LensLarque 9y ago
It looks like you are looking for the V-Model development process used in the industry (e.g. automotive). A typical requirement in this model is handled like this: 1. the high level specification define what is the change about (e.g. implement a hillholder function). 2. architecture phase: you identify which part/module of the system are impacted by the high level requirement. You define what each part will do and you specify how they interface. 3. detailed design phase: each part is formally specified, in the automotive industry we typically use Model based development (Simulink) to specify this phase. 4. implementation: actual coding being done, if you use Simulink this is done by the Simulink/dSpace. A unit test is then performed to check that the detailed design from part 3 has been correctly done. 5. Integration and test: all parts are collected and compiled, and we look that the interfaces are matching. 6. System test: all parts are now tested together against the specifications done in the architecture phase (part 2) and part 1 In the automotive industry, each step can be done by a different person/team/company thus the documentation done in each phase is extremely important to avoid finger pointing in case a problem is detected after delivery.
- virgil_disgr4ce 9y ago
  Excellent, I knew there had to be a ton of history here, but I hadn't known about this specifically. Thank you!
- virgil_disgr4ce 9y ago
  Oh—also—do you know what software out there is already used for managing this complexity? Thanks again!
  - zardo 9y ago
    I think Product Lifecycle Management (PLM) is the buzzword your looking for.
    - virgil_disgr4ce 9y ago
      PLM I'm familiar with, though none of the ones I've seen seem to focus in any particular was on the requirements/specification end of the equation...
      - zardo 9y ago
        Ah okay. So PLM systems would be used to store and manage the requirements, the requirement documents are going to be, at least in my corner of the world... Word and/or Excel templates.
        dfox 9y ago
        Which is only narrow subset of what PLM system does. PLM is generally about tracking what data artifacts (drawings, manufacturer datasheets and so, formal specifications are somewhat secondary to that) are relevant for given assembly and how such subassemblies fit together on high level.
        virgil_disgr4ce 9y ago
digikata 9y ago
If you search for the SEL4 kernel, or the L4 family in general, there's a fair number of papers and presentations on their activity in this area. I don't know if I would characterize it as a particularly fast development process though. https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family
Jtsummers 9y ago
Design to specification can be handled using systems like DOORS or other requirements management software. There’s an interchange format (XML) that many of these support called ReqIF. If you look that up you’ll find an Eclipse based tool (RMF) that is free and let’s you see how linking between requirements and such can be done. I’ve not seen tracing attempted down to the code level though we did do tracing to the test procedures. There’s a plug-in for Event-B in Eclipse that can, in theory, play well with RMF (connect requirements and specs to elements of the formal model). I’ve not spent much time with it but it did seem to do the job.
- virgil_disgr4ce 9y ago
  Ah ha, this is exactly the kind of stuff that I knew must be out there, I but had to find it. Thank you, internet stranger!
  - Jtsummers 9y ago
    No problem. I’m about to embark, with my sister, on a project that will benefit by interacting with these system so I’ve been researching it.
nickpsecurity 9y ago
The thing the specs have in common with your code is they represent entities involved in the systems operation internally or externally to as abstract or concrete detail as you require. They also typically represent the structure and/or order of your system's activities. The abstractions that hide messy details of the machine can let you more easily analyze properties of your system with your eyes, spec/model-checkers, or proof. Some can generate tests from specs. Then, the code's modules should map closely to those abstract actions so you mainky just have to analyze code for isdues that just show up in those parts. The easiest method to start with is Design by Contract plus property-based and fuzz testing. By itself, it lets you specify key properties that are highlighted during a test or runtime failure. Combined with SPARK Ada, you can prove the code is correct against those specs. https://www.eiffel.com/values/design-by-contract/introduction/ https://www.eiffel.com/values/design-by-contract/introductio... http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language)

throwawayjava 9y ago

You might be interested in this study as a way of refining your interests and goals: http://loonwerks.com/publications/pdf/cofer2013fmics.pdf http://loonwerks.com/publications/pdf/cofer2013fmics.pdf It's a big world out there; this has been an active area of research basically since Turing. Many of the "relationship between" questions you ask have their own conference or workshop series. > formal provability IMO the best way to start down this road is to just begin using some of the tools out there -- TLA+, Coq, whatever - and touch base with the community around your choice of tool (conferences, workshops, or even going back to school for a phd). The best way to learn about the strengths and limitations of current software practice is to sit down and churn out code, preferably with a strong mentor. The same is true for proof programming.

LensLarque 9y ago

It looks like you are looking for the V-Model development process used in the industry (e.g. automotive). A typical requirement in this model is handled like this: 1. the high level specification define what is the change about (e.g. implement a hillholder function). 2. architecture phase: you identify which part/module of the system are impacted by the high level requirement. You define what each part will do and you specify how they interface. 3. detailed design phase: each part is formally specified, in the automotive industry we typically use Model based development (Simulink) to specify this phase. 4. implementation: actual coding being done, if you use Simulink this is done by the Simulink/dSpace. A unit test is then performed to check that the detailed design from part 3 has been correctly done. 5. Integration and test: all parts are collected and compiled, and we look that the interfaces are matching. 6. System test: all parts are now tested together against the specifications done in the architecture phase (part 2) and part 1 In the automotive industry, each step can be done by a different person/team/company thus the documentation done in each phase is extremely important to avoid finger pointing in case a problem is detected after delivery.

virgil_disgr4ce 9y ago
Excellent, I knew there had to be a ton of history here, but I hadn't known about this specifically. Thank you!
virgil_disgr4ce 9y ago
Oh—also—do you know what software out there is already used for managing this complexity? Thanks again!
- zardo 9y ago
  I think Product Lifecycle Management (PLM) is the buzzword your looking for.
  - virgil_disgr4ce 9y ago
    PLM I'm familiar with, though none of the ones I've seen seem to focus in any particular was on the requirements/specification end of the equation...
    - zardo 9y ago
      Ah okay. So PLM systems would be used to store and manage the requirements, the requirement documents are going to be, at least in my corner of the world... Word and/or Excel templates.
      - dfox 9y ago
        Which is only narrow subset of what PLM system does. PLM is generally about tracking what data artifacts (drawings, manufacturer datasheets and so, formal specifications are somewhat secondary to that) are relevant for given assembly and how such subassemblies fit together on high level.
        virgil_disgr4ce 9y ago

digikata 9y ago

If you search for the SEL4 kernel, or the L4 family in general, there's a fair number of papers and presentations on their activity in this area. I don't know if I would characterize it as a particularly fast development process though. https://en.wikipedia.org/wiki/L4_microkernel_family https://en.wikipedia.org/wiki/L4_microkernel_family

Jtsummers 9y ago

Design to specification can be handled using systems like DOORS or other requirements management software. There’s an interchange format (XML) that many of these support called ReqIF. If you look that up you’ll find an Eclipse based tool (RMF) that is free and let’s you see how linking between requirements and such can be done. I’ve not seen tracing attempted down to the code level though we did do tracing to the test procedures. There’s a plug-in for Event-B in Eclipse that can, in theory, play well with RMF (connect requirements and specs to elements of the formal model). I’ve not spent much time with it but it did seem to do the job.

virgil_disgr4ce 9y ago
Ah ha, this is exactly the kind of stuff that I knew must be out there, I but had to find it. Thank you, internet stranger!
- Jtsummers 9y ago
  No problem. I’m about to embark, with my sister, on a project that will benefit by interacting with these system so I’ve been researching it.

nickpsecurity 9y ago

The thing the specs have in common with your code is they represent entities involved in the systems operation internally or externally to as abstract or concrete detail as you require. They also typically represent the structure and/or order of your system's activities. The abstractions that hide messy details of the machine can let you more easily analyze properties of your system with your eyes, spec/model-checkers, or proof. Some can generate tests from specs. Then, the code's modules should map closely to those abstract actions so you mainky just have to analyze code for isdues that just show up in those parts. The easiest method to start with is Design by Contract plus property-based and fuzz testing. By itself, it lets you specify key properties that are highlighted during a test or runtime failure. Combined with SPARK Ada, you can prove the code is correct against those specs. https://www.eiffel.com/values/design-by-contract/introduction/ https://www.eiffel.com/values/design-by-contract/introductio... http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf https://en.m.wikipedia.org/wiki/SPARK_(programming_language) https://en.m.wikipedia.org/wiki/SPARK_(programming_language)